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
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
implies: P ⇒ Q,
guard: {T},
so_lambda: λ2x.t[x],
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
so_apply: x[s],
prop: ℙ,
all: ∀x:A. B[x]
Lemmas referenced :
RankEx2-induction,
set_wf,
RankEx2_wf,
all_wf,
list_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
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
lambdaFormation,
sqequalRule,
lambdaEquality,
applyEquality,
because_Cache,
independent_functionElimination,
unionEquality,
cumulativity,
functionEquality,
unionElimination,
setElimination,
rename,
setEquality,
productEquality,
productElimination,
independent_pairEquality,
spreadEquality,
universeEquality
Latex:
\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:
2016_05_16-AM-09_02_32
Last ObjectModification:
2015_12_28-PM-06_51_11
Theory : C-semantics
Home
Index