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