Nuprl Lemma : test-mrec-reduce
test-ind(
         test-aprog(x)
⇒ 1;
         test-iterate(x)
⇒ x.2;
         test-test(x)
⇒ x.3;
         test-afoo(x)
⇒ 4;
         test-bar(x)
⇒ x.5;
         test-xx(x,x)
⇒ x,x.6;
         test-aprop(x)
⇒ 7;
         test-false
⇒ 99;
         test-implies(a,b)
⇒ x,c.c;
         test-box(x,x)
⇒ x,x.9;
         test-diamond(x,x)
⇒ x,x.10)  
test-prop-obj(test-implies(22;33)) ~ test-ind(
                                              test-aprog(x)
⇒ 1;
                                              test-iterate(x)
⇒ x.2;
                                              test-test(x)
⇒ x.3;
                                              test-afoo(x)
⇒ 4;
                                              test-bar(x)
⇒ x.5;
                                              test-xx(x,x)
⇒ x,x.6;
                                              test-aprop(x)
⇒ 7;
                                              test-false
⇒ 99;
                                              test-implies(a,b)
⇒ x,c.c;
                                              test-box(x,x)
⇒ x,x.9;
                                              test-diamond(x,x)
⇒ x,x.10)  
                                     test-prop-obj(33)
Proof
Definitions occuring in Statement : 
test-ind: test-ind, 
test-implies: test-implies(x1;x)
, 
test-prop-obj: test-prop-obj(x)
, 
apply: f a
, 
natural_number: $n
, 
sqequal: s ~ t
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
so_lambda: λ2x.t[x]
, 
member: t ∈ T
, 
top: Top
, 
so_apply: x[s]
, 
so_lambda: λ2x y.t[x; y]
, 
so_apply: x[s1;s2]
, 
so_lambda: so_lambda(x,y,z,w.t[x; y; z; w])
, 
so_apply: x[s1;s2;s3;s4]
Lemmas referenced : 
istype-void
Rules used in proof : 
sqequalSubstitution, 
sqequalRule, 
cut, 
introduction, 
extract_by_obid, 
sqequalHypSubstitution, 
sqequalTransitivity, 
computationStep, 
sqequalReflexivity, 
isectElimination, 
thin, 
isect_memberEquality_alt, 
voidElimination, 
hypothesis
Latex:
test-ind(
                  test-aprog(x){}\mRightarrow{}  1;
                  test-iterate(x){}\mRightarrow{}  x.2;
                  test-test(x){}\mRightarrow{}  x.3;
                  test-afoo(x){}\mRightarrow{}  4;
                  test-bar(x){}\mRightarrow{}  x.5;
                  test-xx(x,x){}\mRightarrow{}  x,x.6;
                  test-aprop(x){}\mRightarrow{}  7;
                  test-false{}\mRightarrow{}  99;
                  test-implies(a,b){}\mRightarrow{}  x,c.c;
                  test-box(x,x){}\mRightarrow{}  x,x.9;
                  test-diamond(x,x){}\mRightarrow{}  x,x.10)   
test-prop-obj(test-implies(22;33))  \msim{}  test-ind(
                                                                                            test-aprog(x){}\mRightarrow{}  1;
                                                                                            test-iterate(x){}\mRightarrow{}  x.2;
                                                                                            test-test(x){}\mRightarrow{}  x.3;
                                                                                            test-afoo(x){}\mRightarrow{}  4;
                                                                                            test-bar(x){}\mRightarrow{}  x.5;
                                                                                            test-xx(x,x){}\mRightarrow{}  x,x.6;
                                                                                            test-aprop(x){}\mRightarrow{}  7;
                                                                                            test-false{}\mRightarrow{}  99;
                                                                                            test-implies(a,b){}\mRightarrow{}  x,c.c;
                                                                                            test-box(x,x){}\mRightarrow{}  x,x.9;
                                                                                            test-diamond(x,x){}\mRightarrow{}  x,x.10)   
                                                                          test-prop-obj(33)
Date html generated:
2019_10_15-AM-10_52_08
Last ObjectModification:
2019_03_22-PM-05_27_42
Theory : tree_1
Home
Index