### Nuprl Lemma : primrec-wf-nat-plus

`∀[P:ℕ+ ⟶ ℙ]. ∀[b:P[1]]. ∀[s:∀n:ℕ+. (P[n] `` P[n + 1])]. ∀[n:ℕ+].  (primrec(n - 1;b;λi,x. (s (i + 1) x)) ∈ P[n])`

Proof

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

Latex:
\mforall{}[P:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[b:P[1]].  \mforall{}[s:\mforall{}n:\mBbbN{}\msupplus{}.  (P[n]  {}\mRightarrow{}  P[n  +  1])].  \mforall{}[n:\mBbbN{}\msupplus{}].
(primrec(n  -  1;b;\mlambda{}i,x.  (s  (i  +  1)  x))  \mmember{}  P[n])

Date html generated: 2016_05_13-PM-03_46_40
Last ObjectModification: 2016_01_14-PM-07_11_32

Theory : call!by!value_2

Home Index