---

Step * of 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)
BY
{ (Reduce 0 THEN Auto) }

---

Latex:

---

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)


By

---

Latex:
(Reduce  0  THEN  Auto)

---

Home Index