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
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 :
RankEx1-induction,
set_wf,
RankEx1_wf,
all_wf,
list_wf,
l_all_wf2,
l_member_wf,
RankEx1_List_wf,
RankEx1_ProdR_wf,
RankEx1_ProdL_wf,
and_wf,
RankEx1_Prod_wf,
RankEx1_Leaf_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,
cumulativity,
functionEquality,
setElimination,
rename,
setEquality,
productEquality,
spreadEquality,
universeEquality
Latex:
\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:
2016_05_16-AM-08_58_36
Last ObjectModification:
2015_12_28-PM-06_52_33
Theory : C-semantics
Home
Index