Nuprl Lemma : test-ind-test-aprop

∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].
  (test-ind(
            test-aprog(x0)⇒ aprog[x0];
            test-iterate(x1)⇒ x2.iterate[x1;x2];
            test-test(x3)⇒ x4.test[x3;x4];
            test-afoo(x5)⇒ afoo[x5];
            test-bar(x6)⇒ x7.bar[x6;x7];
            test-xx(x8,x9)⇒ x10,x11.xx[x8;x9;x10;x11];
            test-aprop(x12)⇒ aprop[x12];
            test-false⇒ false;
            test-implies(x13,x14)⇒ x15,x16.implies[x13;x14;x15;x16];
            test-box(x17,x18)⇒ x19,x20.box[x17;x18;x19;x20];
            test-diamond(x21,x22)⇒ x23,x24.diamond[x21;x22;x23;x24])  
   test-prop-obj(test-aprop(x)) ~ aprop[x])


Proof



Definitions occuring in Statement :  test-ind: test-ind,  test-aprop: test-aprop(x),  test-prop-obj: test-prop-obj(x),  uall: ∀[x:A]. B[x],  top: Top,  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2],  so_apply: x[s],  apply: f a,  sqequal: s ~ t
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  test-ind: test-ind,  test-induction,  mrec_ind: mrec_ind(L;h;x),  test-prop-obj: test-prop-obj(x),  genrec-ap: genrec-ap,  test-aprop: test-aprop(x),  mk-prec: mk-prec(lbl;x),  assert_of_eq_atom,  eqff_to_assert,  decidable__atom_equal,  apply-alist: apply-alist(eq;L;x),  list_ind: list_ind,  test-Spec: test-Spec(),  cons: [a / b],  ifthenelse: if b then t else f fi ,  atom-deq: AtomDeq,  eq_atom: x =a y,  pi1: fst(t),  bfalse: ff,  btrue: tt,  pi2: snd(t),  all: ∀x:A. B[x],  member: t ∈ T,  top: Top,  eqof: eqof(d),  bool_cases_sqequal
Lemmas referenced :  apply_alist_cons_lemma,  istype-void,  istype-top,  test-induction,  assert_of_eq_atom,  eqff_to_assert,  decidable__atom_equal,  bool_cases_sqequal
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  sqequalRule,  cut,  introduction,  extract_by_obid,  sqequalHypSubstitution,  dependent_functionElimination,  thin,  isect_memberEquality_alt,  voidElimination,  hypothesis,  because_Cache,  inhabitedIsType,  hypothesisEquality
Latex:
\mforall{}[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x:Top].
    (test-ind(
                        test-aprog(x0){}\mRightarrow{}  aprog[x0];
                        test-iterate(x1){}\mRightarrow{}  x2.iterate[x1;x2];
                        test-test(x3){}\mRightarrow{}  x4.test[x3;x4];
                        test-afoo(x5){}\mRightarrow{}  afoo[x5];
                        test-bar(x6){}\mRightarrow{}  x7.bar[x6;x7];
                        test-xx(x8,x9){}\mRightarrow{}  x10,x11.xx[x8;x9;x10;x11];
                        test-aprop(x12){}\mRightarrow{}  aprop[x12];
                        test-false{}\mRightarrow{}  false;
                        test-implies(x13,x14){}\mRightarrow{}  x15,x16.implies[x13;x14;x15;x16];
                        test-box(x17,x18){}\mRightarrow{}  x19,x20.box[x17;x18;x19;x20];
                        test-diamond(x21,x22){}\mRightarrow{}  x23,x24.diamond[x21;x22;x23;x24])   
      test-prop-obj(test-aprop(x))  \msim{}  aprop[x])


Date html generated: 2019_10_15-AM-10_51_53
Last ObjectModification: 2019_03_25-PM-01_49_34

Theory : tree_1


Home Index