### Nuprl Lemma : RankEx2-definition

`∀[S,T,A:Type]. ∀[R:A ─→ RankEx2(S;T) ─→ ℙ].`
`  ((∀leaft:T. {x:A| R[x;RankEx2_LeafT(leaft)]} )`
`  `` (∀leafs:S. {x:A| R[x;RankEx2_LeafS(leafs)]} )`
`  `` (∀prod:RankEx2(S;T) × S × T`
`        (let u,u1 = prod in let u1,u2 = u in {x:A| R[x;u1]}  `` {x:A| R[x;RankEx2_Prod(prod)]} ))`
`  `` (∀union:S × RankEx2(S;T) + RankEx2(S;T)`
`        (case union of inl(u) => let u1,u2 = u in {x:A| R[x;u2]}  | inr(u1) => {x:A| R[x;u1]} `
`        `` {x:A| R[x;RankEx2_Union(union)]} ))`
`  `` (∀listprod:(S × RankEx2(S;T)) List`
`        ((∀u∈listprod.let u1,u2 = u in {x:A| R[x;u2]} ) `` {x:A| R[x;RankEx2_ListProd(listprod)]} ))`
`  `` (∀unionlist:T + (RankEx2(S;T) List)`
`        (case unionlist of inl(u) => True | inr(u1) => (∀u∈u1.{x:A| R[x;u]} ) `` {x:A| R[x;RankEx2_UnionList(unionlist)]\000C} ))`
`  `` {∀v:RankEx2(S;T). {x:A| R[x;v]} })`

Proof

Definitions occuring in Statement :  RankEx2_UnionList: `RankEx2_UnionList(unionlist)` RankEx2_ListProd: `RankEx2_ListProd(listprod)` RankEx2_Union: `RankEx2_Union(union)` RankEx2_Prod: `RankEx2_Prod(prod)` RankEx2_LeafS: `RankEx2_LeafS(leafs)` RankEx2_LeafT: `RankEx2_LeafT(leaft)` RankEx2: `RankEx2(S;T)` l_all: `(∀x∈L.P[x])` list: `T List` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` true: `True` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` spread: spread def product: `x:A × B[x]` decide: `case b of inl(x) => s[x] | inr(y) => t[y]` union: `left + right` universe: `Type`
Lemmas :  RankEx2-induction set_wf all_wf list_wf RankEx2_wf true_wf l_all_wf2 l_member_wf RankEx2_UnionList_wf RankEx2_ListProd_wf RankEx2_Union_wf RankEx2_Prod_wf RankEx2_LeafS_wf RankEx2_LeafT_wf
\mforall{}[S,T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  RankEx2(S;T)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}leaft:T.  \{x:A|  R[x;RankEx2\_LeafT(leaft)]\}  )
{}\mRightarrow{}  (\mforall{}leafs:S.  \{x:A|  R[x;RankEx2\_LeafS(leafs)]\}  )
{}\mRightarrow{}  (\mforall{}prod:RankEx2(S;T)  \mtimes{}  S  \mtimes{}  T
(let  u,u1  =  prod  in  let  u1,u2  =  u  in  \{x:A|  R[x;u1]\}    {}\mRightarrow{}  \{x:A|  R[x;RankEx2\_Prod(prod)]\}  ))
{}\mRightarrow{}  (\mforall{}union:S  \mtimes{}  RankEx2(S;T)  +  RankEx2(S;T)
(case  union  of  inl(u)  =>  let  u1,u2  =  u  in  \{x:A|  R[x;u2]\}    |  inr(u1)  =>  \{x:A|  R[x;u1]\}
{}\mRightarrow{}  \{x:A|  R[x;RankEx2\_Union(union)]\}  ))
{}\mRightarrow{}  (\mforall{}listprod:(S  \mtimes{}  RankEx2(S;T))  List
((\mforall{}u\mmember{}listprod.let  u1,u2  =  u  in  \{x:A|  R[x;u2]\}  )  {}\mRightarrow{}  \{x:A|  R[x;RankEx2\_ListProd(listprod)]\}  ))
{}\mRightarrow{}  (\mforall{}unionlist:T  +  (RankEx2(S;T)  List)
(case  unionlist  of  inl(u)  =>  True  |  inr(u1)  =>  (\mforall{}u\mmember{}u1.\{x:A|  R[x;u]\}  )
{}\mRightarrow{}  \{x:A|  R[x;RankEx2\_UnionList(unionlist)]\}  ))
{}\mRightarrow{}  \{\mforall{}v:RankEx2(S;T).  \{x:A|  R[x;v]\}  \})

Date html generated: 2015_07_17-AM-07_50_17
Last ObjectModification: 2015_01_27-AM-09_37_17

Home Index