Nuprl Lemma : test-ind_wf

∀[T:test-Obj() ⟶ TYPE]. ∀[aprog:x:Atom ⟶ T[test-prog-obj(test-aprog(x))]].
∀[iterate:x:test-foo() ⟶ T[test-foo-obj(x)] ⟶ T[test-prog-obj(test-iterate(x))]].
∀[test:x:test-prop() ⟶ T[test-prop-obj(x)] ⟶ T[test-prog-obj(test-test(x))]].
∀[afoo:x:Atom ⟶ T[test-foo-obj(test-afoo(x))]]. ∀[bar:x:test-foo()
                                                       ⟶ T[test-foo-obj(x)]
                                                       ⟶ T[test-foo-obj(test-bar(x))]].
∀[xx:x:test-prop() ⟶ x1:test-prog() ⟶ T[test-prop-obj(x)] ⟶ T[test-prog-obj(x1)] ⟶ T[test-foo-obj(test-xx(x;x1))]].
∀[aprop:x:Atom ⟶ T[test-prop-obj(test-aprop(x))]]. ∀[false:T[test-prop-obj(test-false())]].
∀[implies:x:test-prop()
          ⟶ x1:test-prop()
          ⟶ T[test-prop-obj(x)]
          ⟶ T[test-prop-obj(x1)]
          ⟶ T[test-prop-obj(test-implies(x;x1))]]. ∀[box:x:test-prog()
                                                          ⟶ x1:test-prop()
                                                          ⟶ T[test-prog-obj(x)]
                                                          ⟶ T[test-prop-obj(x1)]
                                                          ⟶ T[test-prop-obj(test-box(x;x1))]].
∀[diamond:x:test-foo()
          ⟶ x1:test-prop()
          ⟶ T[test-foo-obj(x)]
          ⟶ T[test-prop-obj(x1)]
          ⟶ T[test-prop-obj(test-diamond(x;x1))]].
  (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])  ∈ ∀x:test-Obj(). T[x])


Proof



Definitions occuring in Statement :  test-ind: test-ind,  test-diamond: test-diamond(x1;x),  test-box: test-box(x1;x),  test-implies: test-implies(x1;x),  test-false: test-false(),  test-aprop: test-aprop(x),  test-xx: test-xx(x1;x),  test-bar: test-bar(x),  test-afoo: test-afoo(x),  test-test: test-test(x),  test-iterate: test-iterate(x),  test-aprog: test-aprog(x),  test-prop-obj: test-prop-obj(x),  test-foo-obj: test-foo-obj(x),  test-prog-obj: test-prog-obj(x),  test-prop: test-prop(),  test-foo: test-foo(),  test-prog: test-prog(),  test-Obj: test-Obj(),  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2],  so_apply: x[s],  all: ∀x:A. B[x],  member: t ∈ T,  function: x:A ⟶ B[x],  atom: Atom
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  test-ind: test-ind,  all: ∀x:A. B[x],  implies: P ⇒ Q,  so_apply: x[s],  subtype_rel: A ⊆r B,  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2]
Lemmas referenced :  istype-atom,  test-prog-obj_wf,  test-aprog_wf,  test-foo_wf,  test-foo-obj_wf,  test-iterate_wf,  test-prop_wf,  test-prop-obj_wf,  test-test_wf,  test-afoo_wf,  test-bar_wf,  test-prog_wf,  test-xx_wf,  test-aprop_wf,  test-false_wf,  test-implies_wf,  test-box_wf,  test-diamond_wf,  test-Obj_wf,  test-induction
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation_alt,  cut,  sqequalRule,  lambdaEquality_alt,  isectElimination,  hypothesisEquality,  equalityTransitivity,  equalitySymmetry,  hypothesis,  isectIsType,  inhabitedIsType,  functionIsType,  introduction,  extract_by_obid,  TYPEMemberIsType,  applyEquality,  sqequalHypSubstitution,  dependent_functionElimination,  thin,  universeIsType,  because_Cache,  instantiate,  TYPEIsType
Latex:
\mforall{}[T:test-Obj()  {}\mrightarrow{}  TYPE].  \mforall{}[aprog:x:Atom  {}\mrightarrow{}  T[test-prog-obj(test-aprog(x))]].
\mforall{}[iterate:x:test-foo()  {}\mrightarrow{}  T[test-foo-obj(x)]  {}\mrightarrow{}  T[test-prog-obj(test-iterate(x))]].
\mforall{}[test:x:test-prop()  {}\mrightarrow{}  T[test-prop-obj(x)]  {}\mrightarrow{}  T[test-prog-obj(test-test(x))]].
\mforall{}[afoo:x:Atom  {}\mrightarrow{}  T[test-foo-obj(test-afoo(x))]].  \mforall{}[bar:x:test-foo()
                                                                                                              {}\mrightarrow{}  T[test-foo-obj(x)]
                                                                                                              {}\mrightarrow{}  T[test-foo-obj(test-bar(x))]].
\mforall{}[xx:x:test-prop()
          {}\mrightarrow{}  x1:test-prog()
          {}\mrightarrow{}  T[test-prop-obj(x)]
          {}\mrightarrow{}  T[test-prog-obj(x1)]
          {}\mrightarrow{}  T[test-foo-obj(test-xx(x;x1))]].  \mforall{}[aprop:x:Atom  {}\mrightarrow{}  T[test-prop-obj(test-aprop(x))]].
\mforall{}[false:T[test-prop-obj(test-false())]].  \mforall{}[implies:x:test-prop()
                                                                                                      {}\mrightarrow{}  x1:test-prop()
                                                                                                      {}\mrightarrow{}  T[test-prop-obj(x)]
                                                                                                      {}\mrightarrow{}  T[test-prop-obj(x1)]
                                                                                                      {}\mrightarrow{}  T[test-prop-obj(test-implies(x;x1))]].
\mforall{}[box:x:test-prog()
            {}\mrightarrow{}  x1:test-prop()
            {}\mrightarrow{}  T[test-prog-obj(x)]
            {}\mrightarrow{}  T[test-prop-obj(x1)]
            {}\mrightarrow{}  T[test-prop-obj(test-box(x;x1))]].  \mforall{}[diamond:x:test-foo()
                                                                                                            {}\mrightarrow{}  x1:test-prop()
                                                                                                            {}\mrightarrow{}  T[test-foo-obj(x)]
                                                                                                            {}\mrightarrow{}  T[test-prop-obj(x1)]
                                                                                                            {}\mrightarrow{}  T[test-prop-obj(test-diamond(x;x1))]].
    (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])    \mmember{}  \mforall{}x:test-Obj().  T[x])


Date html generated: 2019_10_15-AM-10_51_29
Last ObjectModification: 2019_03_25-PM-01_48_58

Theory : tree_1


Home Index