---

Step * of Lemma dl-complete-induction

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

1
1. [T] : dl-Obj() ⟶ Type
2. ∀x:ℕ. T[prog(atm(x))]
3. ∀x,x1:Prog.  ((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prog(x1)) ⇒ T[y])) ⇒ T[prog((x;x1))])
4. ∀x,x1:Prog.  ((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prog(x1)) ⇒ T[y])) ⇒ T[prog(x ⋃ x1)])
5. ∀x:Prog. ((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ T[prog((x)*)])
6. ∀x:Prop. ((∀y:dl-Obj(). ((↑y ≤ prop(x)) ⇒ T[y])) ⇒ T[prog((x)?)])
7. ∀x:ℕ. T[prop(atm(x))]
8. T[prop(0)]
9. ∀x,x1:Prop.
     ((∀y:dl-Obj(). ((↑y ≤ prop(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop(x ⇒ x1)])
10. ∀x,x1:Prop.
      ((∀y:dl-Obj(). ((↑y ≤ prop(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop(x ∧ x1)])
11. ∀x,x1:Prop.
      ((∀y:dl-Obj(). ((↑y ≤ prop(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop(x ∨ x1)])
12. ∀x:Prog. ∀x1:Prop.
      ((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop([x] x1)])
13. ∀x:Prog. ∀x1:Prop.
      ((∀y:dl-Obj(). ((↑y ≤ prog(x)) ⇒ T[y])) ⇒ (∀y:dl-Obj(). ((↑y ≤ prop(x1)) ⇒ T[y])) ⇒ T[prop(<x> x1)])
14. x : dl-Obj()
⊢ T[x]

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index