Nuprl Lemma : RankEx1-definition

`∀[T,A:Type]. ∀[R:A ─→ RankEx1(T) ─→ ℙ].`
`  ((∀leaf:T. {x:A| R[x;RankEx1_Leaf(leaf)]} )`
`  `` (∀prod:RankEx1(T) × RankEx1(T)`
`        (let u,u1 = prod in {x:A| R[x;u]}  ∧ {x:A| R[x;u1]}  `` {x:A| R[x;RankEx1_Prod(prod)]} ))`
`  `` (∀prodl:T × RankEx1(T). (let u,u1 = prodl in {x:A| R[x;u1]}  `` {x:A| R[x;RankEx1_ProdL(prodl)]} ))`
`  `` (∀prodr:RankEx1(T) × T. (let u,u1 = prodr in {x:A| R[x;u]}  `` {x:A| R[x;RankEx1_ProdR(prodr)]} ))`
`  `` (∀list:RankEx1(T) List. ((∀u∈list.{x:A| R[x;u]} ) `` {x:A| R[x;RankEx1_List(list)]} ))`
`  `` {∀v:RankEx1(T). {x:A| R[x;v]} })`

Proof

Definitions occuring in Statement :  RankEx1_List: `RankEx1_List(list)` RankEx1_ProdR: `RankEx1_ProdR(prodr)` RankEx1_ProdL: `RankEx1_ProdL(prodl)` RankEx1_Prod: `RankEx1_Prod(prod)` RankEx1_Leaf: `RankEx1_Leaf(leaf)` RankEx1: `RankEx1(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` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` spread: spread def product: `x:A × B[x]` universe: `Type`
Lemmas :  RankEx1-induction set_wf all_wf list_wf RankEx1_wf l_all_wf2 l_member_wf RankEx1_List_wf RankEx1_ProdR_wf RankEx1_ProdL_wf RankEx1_Prod_wf RankEx1_Leaf_wf
\mforall{}[T,A:Type].  \mforall{}[R:A  {}\mrightarrow{}  RankEx1(T)  {}\mrightarrow{}  \mBbbP{}].
((\mforall{}leaf:T.  \{x:A|  R[x;RankEx1\_Leaf(leaf)]\}  )
{}\mRightarrow{}  (\mforall{}prod:RankEx1(T)  \mtimes{}  RankEx1(T)
(let  u,u1  =  prod  in  \{x:A|  R[x;u]\}    \mwedge{}  \{x:A|  R[x;u1]\}    {}\mRightarrow{}  \{x:A|  R[x;RankEx1\_Prod(prod)]\}  ))
{}\mRightarrow{}  (\mforall{}prodl:T  \mtimes{}  RankEx1(T)
(let  u,u1  =  prodl  in  \{x:A|  R[x;u1]\}    {}\mRightarrow{}  \{x:A|  R[x;RankEx1\_ProdL(prodl)]\}  ))
{}\mRightarrow{}  (\mforall{}prodr:RankEx1(T)  \mtimes{}  T
(let  u,u1  =  prodr  in  \{x:A|  R[x;u]\}    {}\mRightarrow{}  \{x:A|  R[x;RankEx1\_ProdR(prodr)]\}  ))
{}\mRightarrow{}  (\mforall{}list:RankEx1(T)  List.  ((\mforall{}u\mmember{}list.\{x:A|  R[x;u]\}  )  {}\mRightarrow{}  \{x:A|  R[x;RankEx1\_List(list)]\}  ))
{}\mRightarrow{}  \{\mforall{}v:RankEx1(T).  \{x:A|  R[x;v]\}  \})

Date html generated: 2015_07_17-AM-07_48_34
Last ObjectModification: 2015_01_27-AM-09_38_30

Home Index