---

Step * of Lemma test-ind-test-aprog

∀[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-prog-obj(test-aprog(x)) ~ aprog[x])
BY
{ MrecIndReduce }

---

Latex:

---

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-prog-obj(test-aprog(x))  \msim{}  aprog[x])


By

---

Latex:
MrecIndReduce

---

Home Index