---

Step * of Lemma dl-induction

∀[T:dl-Obj() ⟶ TYPE]
  ((∀x:ℕ. T[prog(atm(x))])
  ⇒ (∀x,x1:Prog.  (T[prog(x)] ⇒ T[prog(x1)] ⇒ T[prog((x;x1))]))
  ⇒ (∀x,x1:Prog.  (T[prog(x)] ⇒ T[prog(x1)] ⇒ T[prog(x ⋃ x1)]))
  ⇒ (∀x:Prog. (T[prog(x)] ⇒ T[prog((x)*)]))
  ⇒ (∀x:Prop. (T[prop(x)] ⇒ T[prog((x)?)]))
  ⇒ (∀x:ℕ. T[prop(atm(x))])
  ⇒ T[prop(0)]
  ⇒ (∀x,x1:Prop.  (T[prop(x)] ⇒ T[prop(x1)] ⇒ T[prop(x ⇒ x1)]))
  ⇒ (∀x,x1:Prop.  (T[prop(x)] ⇒ T[prop(x1)] ⇒ T[prop(x ∧ x1)]))
  ⇒ (∀x,x1:Prop.  (T[prop(x)] ⇒ T[prop(x1)] ⇒ T[prop(x ∨ x1)]))
  ⇒ (∀x:Prog. ∀x1:Prop.  (T[prog(x)] ⇒ T[prop(x1)] ⇒ T[prop([x] x1)]))
  ⇒ (∀x:Prog. ∀x1:Prop.  (T[prog(x)] ⇒ T[prop(x1)] ⇒ T[prop(<x> x1)]))
  ⇒ (∀x:dl-Obj(). T[x]))
BY
{ ProveMobjInduction }

---

Latex:

---

Latex:
\mforall{}[T:dl-Obj()  {}\mrightarrow{}  TYPE]
    ((\mforall{}x:\mBbbN{}.  T[prog(atm(x))])
    {}\mRightarrow{}  (\mforall{}x,x1:Prog.    (T[prog(x)]  {}\mRightarrow{}  T[prog(x1)]  {}\mRightarrow{}  T[prog((x;x1))]))
    {}\mRightarrow{}  (\mforall{}x,x1:Prog.    (T[prog(x)]  {}\mRightarrow{}  T[prog(x1)]  {}\mRightarrow{}  T[prog(x  \mcup{}  x1)]))
    {}\mRightarrow{}  (\mforall{}x:Prog.  (T[prog(x)]  {}\mRightarrow{}  T[prog((x)*)]))
    {}\mRightarrow{}  (\mforall{}x:Prop.  (T[prop(x)]  {}\mRightarrow{}  T[prog((x)?)]))
    {}\mRightarrow{}  (\mforall{}x:\mBbbN{}.  T[prop(atm(x))])
    {}\mRightarrow{}  T[prop(0)]
    {}\mRightarrow{}  (\mforall{}x,x1:Prop.    (T[prop(x)]  {}\mRightarrow{}  T[prop(x1)]  {}\mRightarrow{}  T[prop(x  {}\mRightarrow{}  x1)]))
    {}\mRightarrow{}  (\mforall{}x,x1:Prop.    (T[prop(x)]  {}\mRightarrow{}  T[prop(x1)]  {}\mRightarrow{}  T[prop(x  \mwedge{}  x1)]))
    {}\mRightarrow{}  (\mforall{}x,x1:Prop.    (T[prop(x)]  {}\mRightarrow{}  T[prop(x1)]  {}\mRightarrow{}  T[prop(x  \mvee{}  x1)]))
    {}\mRightarrow{}  (\mforall{}x:Prog.  \mforall{}x1:Prop.    (T[prog(x)]  {}\mRightarrow{}  T[prop(x1)]  {}\mRightarrow{}  T[prop([x]  x1)]))
    {}\mRightarrow{}  (\mforall{}x:Prog.  \mforall{}x1:Prop.    (T[prog(x)]  {}\mRightarrow{}  T[prop(x1)]  {}\mRightarrow{}  T[prop(<x>  x1)]))
    {}\mRightarrow{}  (\mforall{}x:dl-Obj().  T[x]))


By

---

Latex:
ProveMobjInduction

---

Home Index