Proof of Nuprl Lemma : dl-complete-induction

Step * 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()
⊢ T[x]
BY
{ (InstLemma `dl-induction` [⌜λ₂x.∀y:dl-Obj(). ((↑y ≤ x) ⇒ T[y])⌝]⋅
   THEN Auto
   THEN Try ((DloLeReduce (-1)
              THEN (RW assert_pushdownC (-1) THENA Auto)
              THEN (RWO "assert-dlo_eq" (-1) THENA Auto)
              THEN SplitOrHyps
              THEN 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()
15. ∀x,y:dl-Obj().  ((↑y ≤ x) ⇒ T[y])
⊢ T[x]

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() \mvdash{} T[x] By Latex: (InstLemma `dl-induction` [\mkleeneopen{}\mlambda{}\msubtwo{}x.\mforall{}y:dl-Obj(). ((\muparrow{}y \mleq{} x) {}\mRightarrow{} T[y])\mkleeneclose{}]\mcdot{} THEN Auto THEN Try ((DloLeReduce (-1) THEN (RW assert\_pushdownC (-1) THENA Auto) THEN (RWO "assert-dlo\_eq" (-1) THENA Auto) THEN SplitOrHyps THEN Auto))) Home Index