---

Step * of Lemma complete_nat_ind

∀[P:ℕ ⟶ ℙ]. ((∀i:ℕ. ((∀j:ℕi. P[j]) ⇒ P[i])) ⇒ (∀i:ℕ. P[i]))
BY
{ (Auto THEN Assert ⌜∀n:ℕ. ∀i:ℕn.  P[i]⌝⋅) }

1
.....assertion..... 
1. [P] : ℕ ⟶ ℙ
2. ∀i:ℕ. ((∀j:ℕi. P[j]) ⇒ P[i])@i
3. i : ℕ@i
⊢ ∀n:ℕ. ∀i:ℕn.  P[i]

2
1. [P] : ℕ ⟶ ℙ
2. ∀i:ℕ. ((∀j:ℕi. P[j]) ⇒ P[i])@i
3. i : ℕ@i
4. ∀n:ℕ. ∀i:ℕn.  P[i]
⊢ P[i]

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}i.  P[j])  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  P[i]))


By

---

Latex:
(Auto  THEN  Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}i:\mBbbN{}n.    P[i]\mkleeneclose{}\mcdot{})

---

Home Index