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. : ℕ@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