Step
*
of Lemma
cont-induction
∀[P:ℕ ⟶ ℙ]. (P[0]
⇒ (∀n:ℕ. (P[n]
⇒ P[n + 1]))
⇒ (∀n:ℕ. P[n]))
BY
{ (Auto THEN (InstLemma `cont-induction-lemma` [⌜P⌝;⌜n⌝;⌜0⌝]⋅ THENA Auto)) }
1
1. [P] : ℕ ⟶ ℙ
2. P[0]@i
3. ∀n:ℕ. (P[n]
⇒ P[n + 1])@i
4. n : ℕ@i
5. P[n + 0]
⊢ P[n]
Latex:
Latex:
\mforall{}[P:\mBbbN{} {}\mrightarrow{} \mBbbP{}]. (P[0] {}\mRightarrow{} (\mforall{}n:\mBbbN{}. (P[n] {}\mRightarrow{} P[n + 1])) {}\mRightarrow{} (\mforall{}n:\mBbbN{}. P[n]))
By
Latex:
(Auto THEN (InstLemma `cont-induction-lemma` [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]\mcdot{} THENA Auto))
Home
Index