### Nuprl Lemma : div_nat_induction-ext

`∀b:{b:ℤ| 1 < b} . ∀[P:ℕ ⟶ ℙ]. (P[0] `` (∀i:ℕ+. (P[i ÷ b] `` P[i])) `` (∀i:ℕ. P[i]))`

Proof

Definitions occuring in Statement :  nat_plus: `ℕ+` nat: `ℕ` less_than: `a < b` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` divide: `n ÷ m` natural_number: `\$n` int: `ℤ`
Definitions unfolded in proof :  squash: `↓T` or: `P ∨ Q` guard: `{T}` prop: `ℙ` has-value: `(a)↓` implies: `P `` Q` all: `∀x:A. B[x]` and: `P ∧ Q` strict4: `strict4(F)` uimplies: `b supposing a` so_apply: `x[s]` top: `Top` so_lambda: `λ2x.t[x]` so_apply: `x[s1;s2;s3;s4]` so_lambda: `so_lambda(x,y,z,w.t[x; y; z; w])` uall: `∀[x:A]. B[x]` decidable__int_equal decidable__equal_int so_apply: `x[s1;s2]` div_nat_induction member: `t ∈ T`
Lemmas referenced :  is-exception_wf base_wf has-value_wf_base equal_wf top_wf lifting-strict-int_eq div_nat_induction decidable__int_equal decidable__equal_int
Rules used in proof :  inlFormation exceptionSqequal imageElimination imageMemberEquality because_Cache inrFormation decideExceptionCases closedConclusion baseApply independent_functionElimination dependent_functionElimination sqleReflexivity unionElimination unionEquality equalitySymmetry equalityTransitivity hypothesisEquality callbyvalueDecide lambdaFormation independent_pairFormation independent_isectElimination voidEquality voidElimination isect_memberEquality baseClosed isectElimination sqequalHypSubstitution thin sqequalRule hypothesis extract_by_obid instantiate cut sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution introduction

Latex:
\mforall{}b:\{b:\mBbbZ{}|  1  <  b\}  .  \mforall{}[P:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}].  (P[0]  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}\msupplus{}.  (P[i  \mdiv{}  b]  {}\mRightarrow{}  P[i]))  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}.  P[i]))

Date html generated: 2018_05_21-PM-07_49_34
Last ObjectModification: 2018_05_19-AM-07_44_27

Theory : general

Home Index