### Nuprl Lemma : complete_nat_ind

`∀[P:ℕ ⟶ ℙ]. ((∀i:ℕ. ((∀j:ℕi. P[j]) `` P[i])) `` (∀i:ℕ. P[i]))`

Proof

Definitions occuring in Statement :  int_seg: `{i..j-}` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` natural_number: `\$n`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` implies: `P `` Q` all: `∀x:A. B[x]` member: `t ∈ T` prop: `ℙ` so_lambda: `λ2x.t[x]` nat: `ℕ` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` le: `A ≤ B` and: `P ∧ Q` less_than': `less_than'(a;b)` false: `False` not: `¬A` int_seg: `{i..j-}` lelt: `i ≤ j < k` guard: `{T}` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` top: `Top` true: `True` less_than: `a < b` sq_stable: `SqStable(P)` squash: `↓T`
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut lemma_by_obid hypothesis sqequalHypSubstitution isectElimination thin sqequalRule lambdaEquality functionEquality natural_numberEquality setElimination rename hypothesisEquality applyEquality independent_isectElimination independent_pairFormation because_Cache universeEquality cumulativity productElimination independent_functionElimination voidElimination dependent_functionElimination intEquality introduction dependent_set_memberEquality unionElimination addEquality minusEquality isect_memberEquality voidEquality imageMemberEquality baseClosed imageElimination multiplyEquality

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  ((\mforall{}i:\mBbbN{}.  ((\mforall{}j:\mBbbN{}i.  P[j])  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  P[i]))

Date html generated: 2016_05_13-PM-04_02_56
Last ObjectModification: 2016_01_14-PM-07_24_48

Theory : int_1

Home Index