Nuprl Lemma : cont-induction-ext

[P:ℕ ⟶ ℙ]. (P[0]  (∀n:ℕ(P[n]  P[n 1]))  (∀n:ℕP[n]))


Proof




Definitions occuring in Statement :  nat: uall: [x:A]. B[x] prop: so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] add: m natural_number: $n
Definitions unfolded in proof :  member: t ∈ T cont-induction cont-induction-lemma primrec-induction
Lemmas referenced :  cont-induction cont-induction-lemma primrec-induction
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution equalityTransitivity equalitySymmetry

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



Date html generated: 2018_05_21-PM-06_59_48
Last ObjectModification: 2018_05_19-PM-04_42_03

Theory : general


Home Index