---

Step * of Lemma test-ind-test-implies

∀[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1: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-implies(x;x1)) 
  ~ implies[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])  
                 test-prop-obj(x);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(x1)])
BY
{ MrecIndReduce }

---

Latex:

---

Latex:
\mforall{}[aprog,iterate,test,afoo,bar,xx,aprop,false,implies,box,diamond,x,x1: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-implies(x;x1)) 
    \msim{}  implies[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])   
                                  test-prop-obj(x);... 
                                                                    test-prop-obj(x1)])


By

---

Latex:
MrecIndReduce

---

Home Index