---

Step * 2 of Lemma complete_nat_ind


1. [P] : ℕ ⟶ ℙ
2. ∀i:ℕ. ((∀j:ℕi. P[j]) ⇒ P[i])@i
3. i : ℕ@i
4. ∀n:ℕ. ∀i:ℕn.  P[i]
⊢ P[i]
BY
{ (InstHyp [⌜i + 1⌝;⌜i⌝] (-1)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [P]  :  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  \mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}i.  P[j])  {}\mRightarrow{}  P[i])@i
3.  i  :  \mBbbN{}@i
4.  \mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    P[i]
\mvdash{}  P[i]


By

---

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

---

Home Index