---

Step * of Lemma test-induction

∀[T:test-Obj() ⟶ TYPE]
  ((∀x:Atom. T[test-prog-obj(test-aprog(x))])
  ⇒ (∀x:test-foo(). (T[test-foo-obj(x)] ⇒ T[test-prog-obj(test-iterate(x))]))
  ⇒ (∀x:test-prop(). (T[test-prop-obj(x)] ⇒ T[test-prog-obj(test-test(x))]))
  ⇒ (∀x:Atom. T[test-foo-obj(test-afoo(x))])
  ⇒ (∀x:test-foo(). (T[test-foo-obj(x)] ⇒ T[test-foo-obj(test-bar(x))]))
  ⇒ (∀x:test-prop(). ∀x1:test-prog().  (T[test-prop-obj(x)] ⇒ T[test-prog-obj(x1)] ⇒ T[test-foo-obj(test-xx(x;x1))]))
  ⇒ (∀x:Atom. T[test-prop-obj(test-aprop(x))])
  ⇒ T[test-prop-obj(test-false())]
  ⇒ (∀x,x1:test-prop().  (T[test-prop-obj(x)] ⇒ T[test-prop-obj(x1)] ⇒ T[test-prop-obj(test-implies(x;x1))]))
  ⇒ (∀x:test-prog(). ∀x1:test-prop().
        (T[test-prog-obj(x)] ⇒ T[test-prop-obj(x1)] ⇒ T[test-prop-obj(test-box(x;x1))]))
  ⇒ (∀x:test-foo(). ∀x1:test-prop().
        (T[test-foo-obj(x)] ⇒ T[test-prop-obj(x1)] ⇒ T[test-prop-obj(test-diamond(x;x1))]))
  ⇒ (∀x:test-Obj(). T[x]))
BY
{ ProveMobjInduction }

---

Latex:

---

Latex:
\mforall{}[T:test-Obj()  {}\mrightarrow{}  TYPE]
    ((\mforall{}x:Atom.  T[test-prog-obj(test-aprog(x))])
    {}\mRightarrow{}  (\mforall{}x:test-foo().  (T[test-foo-obj(x)]  {}\mRightarrow{}  T[test-prog-obj(test-iterate(x))]))
    {}\mRightarrow{}  (\mforall{}x:test-prop().  (T[test-prop-obj(x)]  {}\mRightarrow{}  T[test-prog-obj(test-test(x))]))
    {}\mRightarrow{}  (\mforall{}x:Atom.  T[test-foo-obj(test-afoo(x))])
    {}\mRightarrow{}  (\mforall{}x:test-foo().  (T[test-foo-obj(x)]  {}\mRightarrow{}  T[test-foo-obj(test-bar(x))]))
    {}\mRightarrow{}  (\mforall{}x:test-prop().  \mforall{}x1:test-prog().
                (T[test-prop-obj(x)]  {}\mRightarrow{}  T[test-prog-obj(x1)]  {}\mRightarrow{}  T[test-foo-obj(test-xx(x;x1))]))
    {}\mRightarrow{}  (\mforall{}x:Atom.  T[test-prop-obj(test-aprop(x))])
    {}\mRightarrow{}  T[test-prop-obj(test-false())]
    {}\mRightarrow{}  (\mforall{}x,x1:test-prop().
                (T[test-prop-obj(x)]  {}\mRightarrow{}  T[test-prop-obj(x1)]  {}\mRightarrow{}  T[test-prop-obj(test-implies(x;x1))]))
    {}\mRightarrow{}  (\mforall{}x:test-prog().  \mforall{}x1:test-prop().
                (T[test-prog-obj(x)]  {}\mRightarrow{}  T[test-prop-obj(x1)]  {}\mRightarrow{}  T[test-prop-obj(test-box(x;x1))]))
    {}\mRightarrow{}  (\mforall{}x:test-foo().  \mforall{}x1:test-prop().
                (T[test-foo-obj(x)]  {}\mRightarrow{}  T[test-prop-obj(x1)]  {}\mRightarrow{}  T[test-prop-obj(test-diamond(x;x1))]))
    {}\mRightarrow{}  (\mforall{}x:test-Obj().  T[x]))


By

---

Latex:
ProveMobjInduction

---

Home Index