---

Step * of Lemma rec-nat-induction

∀[P:ℕ ⟶ ℙ]. (∀[n:ℕ]. (P[n] ⇒ P[n + 1])) ⇒ (∀[n:ℕ]. P[n]) supposing Top ⊆r P[0]
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN RenameVar `f' (-1)) }

1
1. [P] : ℕ ⟶ ℙ
2. Top ⊆r P[0]
3. f : ∀[n:ℕ]. (P[n] ⇒ P[n + 1])@i
⊢ ∀[n:ℕ]. P[n]

---

Latex:

---

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (\mforall{}[n:\mBbbN{}].  (P[n]  {}\mRightarrow{}  P[n  +  1]))  {}\mRightarrow{}  (\mforall{}[n:\mBbbN{}].  P[n])  supposing  Top  \msubseteq{}r  P[0]


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))  THEN  RenameVar  `f'  (-1))

---

Home Index