Nuprl Lemma : accum-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: P ⇒ Q,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n
Definitions unfolded in proof :
member: t ∈ T,
accum-induction,
accum-induction-lemma,
primrec-induction
Lemmas referenced :
accum-induction,
accum-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_56
Last ObjectModification:
2018_05_19-PM-04_42_14
Theory : general
Home
Index