---

Step * 1 1 of Lemma dl-complete-induction


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()
15. ∀x,y:dl-Obj().  ((↑y ≤ x) ⇒ T[y])
⊢ T[x]
BY
{ (InstHyp [⌜x⌝;⌜x⌝] (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  dl-Obj()  {}\mrightarrow{}  Type
2.  \mforall{}x:\mBbbN{}.  T[prog(atm(x))]
3.  \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))])
4.  \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)])
5.  \mforall{}x:Prog.  ((\mforall{}y:dl-Obj().  ((\muparrow{}y  \mleq{}  prog(x))  {}\mRightarrow{}  T[y]))  {}\mRightarrow{}  T[prog((x)*)])
6.  \mforall{}x:Prop.  ((\mforall{}y:dl-Obj().  ((\muparrow{}y  \mleq{}  prop(x))  {}\mRightarrow{}  T[y]))  {}\mRightarrow{}  T[prog((x)?)])
7.  \mforall{}x:\mBbbN{}.  T[prop(atm(x))]
8.  T[prop(0)]
9.  \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)])
10.  \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)])
11.  \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)])
12.  \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)])
13.  \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)])
14.  x  :  dl-Obj()
15.  \mforall{}x,y:dl-Obj().    ((\muparrow{}y  \mleq{}  x)  {}\mRightarrow{}  T[y])
\mvdash{}  T[x]


By

---

Latex:
(InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)

---

Home Index