Nuprl Lemma : nat_ind_a

[P:ℕ ⟶ ℙ{k}]. (P[0]  (∀i:ℕ+(P[i 1]  P[i]))  {∀i:ℕP[i]})


Proof




Definitions occuring in Statement :  nat_plus: + nat: uall: [x:A]. B[x] prop: guard: {T} so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] subtract: m natural_number: $n
Definitions unfolded in proof :  guard: {T} uall: [x:A]. B[x] implies:  Q all: x:A. B[x] member: t ∈ T nat_plus: + nat: le: A ≤ B and: P ∧ Q decidable: Dec(P) or: P ∨ Q iff: ⇐⇒ Q not: ¬A rev_implies:  Q false: False prop: uiff: uiff(P;Q) uimplies: supposing a subtract: m subtype_rel: A ⊆B less_than': less_than'(a;b) true: True so_apply: x[s] so_lambda: λ2x.t[x] top: Top
Lemmas referenced :  decidable__lt false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel less_than_wf add-subtract-cancel primrec-wf nat_wf all_wf nat_plus_wf subtract_wf decidable__le not-le-2 less-iff-le minus-minus add-swap le_wf nat_plus_subtype_nat
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation lambdaFormation rename cut hypothesis sqequalHypSubstitution dependent_functionElimination thin dependent_set_memberEquality addEquality setElimination hypothesisEquality natural_numberEquality productElimination lemma_by_obid unionElimination independent_pairFormation voidElimination independent_functionElimination independent_isectElimination isectElimination applyEquality because_Cache minusEquality introduction instantiate lambdaEquality cumulativity universeEquality functionEquality isect_memberEquality voidEquality intEquality

Latex:
\mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}\{k\}].  (P[0]  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}\msupplus{}.  (P[i  -  1]  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  \{\mforall{}i:\mBbbN{}.  P[i]\})



Date html generated: 2016_05_13-PM-03_47_07
Last ObjectModification: 2015_12_26-AM-09_58_08

Theory : call!by!value_2


Home Index