Nuprl Lemma : def-cont-induction-lemma-ext
∀[P:ℕ ⟶ ℙ]
((∀n:ℕ. (P[n] ⇒ P[n + 1])) ⇒ (∀x:ℤ List. ∀[n,m:ℕ]. P[n] ⇒ P[m] supposing (x = [n, m) ∈ (ℤ List)) ∧ (n ≤ m)))
Proof
Definitions occuring in Statement :
from-upto: [n, m),
list: T List,
nat: ℕ,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
prop: ℙ,
so_apply: x[s],
le: A ≤ B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x],
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
member: t ∈ T,
def-cont-induction-lemma,
list_induction,
sq_stable__and,
sq_stable__equal
Lemmas referenced :
def-cont-induction-lemma,
list_induction,
sq_stable__and,
sq_stable__equal
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{}]
((\mforall{}n:\mBbbN{}. (P[n] {}\mRightarrow{} P[n + 1]))
{}\mRightarrow{} (\mforall{}x:\mBbbZ{} List. \mforall{}[n,m:\mBbbN{}]. P[n] {}\mRightarrow{} P[m] supposing (x = [n, m)) \mwedge{} (n \mleq{} m)))
Date html generated:
2018_05_21-PM-07_00_03
Last ObjectModification:
2018_05_19-PM-04_42_26
Theory : general
Home
Index