---

Step * of Lemma test-ind_wf_definition

∀[A,B,C:TYPE]. ∀[aprog:x:Atom ⟶ A]. ∀[iterate:x:test-foo() ⟶ B ⟶ A]. ∀[test:x:test-prop() ⟶ C ⟶ A].
∀[afoo:x:Atom ⟶ B]. ∀[bar:x:test-foo() ⟶ B ⟶ B]. ∀[xx:x:test-prop() ⟶ x1:test-prog() ⟶ C ⟶ A ⟶ B]. ∀[aprop:x:Atom
                                                                                                                  ⟶ C].
∀[false:C]. ∀[implies:x:test-prop() ⟶ x1:test-prop() ⟶ C ⟶ C ⟶ C]. ∀[box:x:test-prog()
                                                                             ⟶ x1:test-prop()
                                                                             ⟶ A
                                                                             ⟶ C
                                                                             ⟶ C]. ∀[diamond:x:test-foo()
                                                                                              ⟶ x1:test-prop()
                                                                                              ⟶ B
                                                                                              ⟶ C
                                                                                              ⟶ C].
  (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])  ∈ d:test-Obj() ⟶ if test-kind(d) =a "prog"
                                                                                           then A
                                                                                         if test-kind(d) =a "foo" then B
                                                                                         else C
                                                                                         fi )
BY
{ MrecIndDef }

---

Latex:

---

Latex:
\mforall{}[A,B,C:TYPE].  \mforall{}[aprog:x:Atom  {}\mrightarrow{}  A].  \mforall{}[iterate:x:test-foo()  {}\mrightarrow{}  B  {}\mrightarrow{}  A].  \mforall{}[test:x:test-prop()
                                                                                                                                                              {}\mrightarrow{}  C
                                                                                                                                                              {}\mrightarrow{}  A].
\mforall{}[afoo:x:Atom  {}\mrightarrow{}  B].  \mforall{}[bar:x:test-foo()  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[xx:x:test-prop()
                                                                                                                  {}\mrightarrow{}  x1:test-prog()
                                                                                                                  {}\mrightarrow{}  C
                                                                                                                  {}\mrightarrow{}  A
                                                                                                                  {}\mrightarrow{}  B].  \mforall{}[aprop:x:Atom  {}\mrightarrow{}  C].  \mforall{}[false:C].
\mforall{}[implies:x:test-prop()  {}\mrightarrow{}  x1:test-prop()  {}\mrightarrow{}  C  {}\mrightarrow{}  C  {}\mrightarrow{}  C].  \mforall{}[box:x:test-prog()
                                                                                                                                  {}\mrightarrow{}  x1:test-prop()
                                                                                                                                  {}\mrightarrow{}  A
                                                                                                                                  {}\mrightarrow{}  C
                                                                                                                                  {}\mrightarrow{}  C].  \mforall{}[diamond:x:test-foo()
                                                                                                                                                                    {}\mrightarrow{}  x1:test-prop()
                                                                                                                                                                    {}\mrightarrow{}  B
                                                                                                                                                                    {}\mrightarrow{}  C
                                                                                                                                                                    {}\mrightarrow{}  C].
    (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{}  d:test-Obj()
      {}\mrightarrow{}  if  test-kind(d)  =a  "prog"  then  A
            if  test-kind(d)  =a  "foo"  then  B
            else  C
            fi  )


By

---

Latex:
MrecIndDef

---

Home Index