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