Nuprl Lemma : RankEx1_ind_wf_simple
∀[T,A:Type]. ∀[v:RankEx1(T)]. ∀[Leaf:leaf:T ⟶ A]. ∀[Prod:prod:(RankEx1(T) × RankEx1(T))
                                                          ⟶ let u,u1 = prod 
                                                             in A ∧ A
                                                          ⟶ A]. ∀[ProdL:prodl:(T × RankEx1(T))
                                                                         ⟶ let u,u1 = prodl 
                                                                            in A
                                                                         ⟶ A]. ∀[ProdR:prodr:(RankEx1(T) × T)
                                                                                        ⟶ let u,u1 = prodr 
                                                                                           in A
                                                                                        ⟶ A].
∀[List:list:(RankEx1(T) List) ⟶ (∀u∈list.A) ⟶ A].
  (RankEx1_ind(v;
               RankEx1_Leaf(leaf)
⇒ Leaf[leaf];
               RankEx1_Prod(prod)
⇒ rec1.Prod[prod;rec1];
               RankEx1_ProdL(prodl)
⇒ rec2.ProdL[prodl;rec2];
               RankEx1_ProdR(prodr)
⇒ rec3.ProdR[prodr;rec3];
               RankEx1_List(list)
⇒ rec4.List[list;rec4])  ∈ A)
Proof
Definitions occuring in Statement : 
RankEx1_ind: RankEx1_ind, 
RankEx1: RankEx1(T)
, 
l_all: (∀x∈L.P[x])
, 
list: T List
, 
uall: ∀[x:A]. B[x]
, 
so_apply: x[s1;s2]
, 
so_apply: x[s]
, 
and: P ∧ Q
, 
member: t ∈ T
, 
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
, 
so_lambda: λ2x y.t[x; y]
, 
so_apply: x[s1;s2]
, 
subtype_rel: A ⊆r B
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
prop: ℙ
, 
uimplies: b supposing a
, 
all: ∀x:A. B[x]
, 
true: True
, 
and: P ∧ Q
, 
implies: P 
⇒ Q
, 
guard: {T}
Lemmas referenced : 
RankEx1_ind_wf, 
true_wf, 
RankEx1_wf, 
subtype_rel_dep_function, 
and_wf, 
set_wf, 
subtype_rel_product, 
list_wf, 
l_all_wf2, 
l_member_wf, 
subtype-l_all
Rules used in proof : 
cut, 
lemma_by_obid, 
sqequalSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isect_memberFormation, 
hypothesis, 
sqequalHypSubstitution, 
isectElimination, 
thin, 
hypothesisEquality, 
sqequalRule, 
lambdaEquality, 
applyEquality, 
because_Cache, 
setEquality, 
independent_isectElimination, 
lambdaFormation, 
dependent_set_memberEquality, 
natural_numberEquality, 
productEquality, 
functionEquality, 
spreadEquality, 
productElimination, 
setElimination, 
rename, 
equalityTransitivity, 
equalitySymmetry, 
universeEquality
Latex:
\mforall{}[T,A:Type].  \mforall{}[v:RankEx1(T)].  \mforall{}[Leaf:leaf:T  {}\mrightarrow{}  A].  \mforall{}[Prod:prod:(RankEx1(T)  \mtimes{}  RankEx1(T))
                                                                                                                    {}\mrightarrow{}  let  u,u1  =  prod 
                                                                                                                          in  A  \mwedge{}  A
                                                                                                                    {}\mrightarrow{}  A].  \mforall{}[ProdL:prodl:(T  \mtimes{}  RankEx1(T))
                                                                                                                                                  {}\mrightarrow{}  let  u,u1  =  prodl 
                                                                                                                                                        in  A
                                                                                                                                                  {}\mrightarrow{}  A].
\mforall{}[ProdR:prodr:(RankEx1(T)  \mtimes{}  T)  {}\mrightarrow{}  let  u,u1  =  prodr  in  A  {}\mrightarrow{}  A].  \mforall{}[List:list:(RankEx1(T)  List)
                                                                                                                                            {}\mrightarrow{}  (\mforall{}u\mmember{}list.A)
                                                                                                                                            {}\mrightarrow{}  A].
    (RankEx1\_ind(v;
                              RankEx1\_Leaf(leaf){}\mRightarrow{}  Leaf[leaf];
                              RankEx1\_Prod(prod){}\mRightarrow{}  rec1.Prod[prod;rec1];
                              RankEx1\_ProdL(prodl){}\mRightarrow{}  rec2.ProdL[prodl;rec2];
                              RankEx1\_ProdR(prodr){}\mRightarrow{}  rec3.ProdR[prodr;rec3];
                              RankEx1\_List(list){}\mRightarrow{}  rec4.List[list;rec4])    \mmember{}  A)
Date html generated:
2016_05_16-AM-08_58_49
Last ObjectModification:
2015_12_28-PM-06_51_51
Theory : C-semantics
Home
Index