### Nuprl Lemma : simple-primrec-add

`∀[b,F:Top]. ∀[n,m:ℕ].  (primrec(n + m;b;λi.F) ~ primrec(n;primrec(m;b;λi.F);λi.F))`

Proof

Definitions occuring in Statement :  primrec: `primrec(n;b;c)` nat: `ℕ` uall: `∀[x:A]. B[x]` top: `Top` lambda: `λx.A[x]` add: `n + m` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` guard: `{T}` uimplies: `b supposing a` prop: `ℙ` all: `∀x:A. B[x]` top: `Top` decidable: `Dec(P)` or: `P ∨ Q` iff: `P `⇐⇒` Q` and: `P ∧ Q` not: `¬A` rev_implies: `P `` Q` uiff: `uiff(P;Q)` subtract: `n - m` subtype_rel: `A ⊆r B` le: `A ≤ B` less_than': `less_than'(a;b)` true: `True` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` nat_plus: `ℕ+` less_than: `a < b` squash: `↓T`
Lemmas referenced :  nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf primrec0_lemma zero-add decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul minus-one-mul-top minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel nat_wf top_wf eq_int_wf bool_wf equal-wf-T-base assert_wf eqtt_to_assert assert_of_eq_int le_weakening eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base iff_transitivity bnot_wf not_wf equal-wf-base int_subtype_base iff_weakening_uiff assert_of_bnot minus-zero add-mul-special zero-mul not-equal-implies-less subtype_rel_self le_reflexive one-mul two-mul mul-distributes-right omega-shadow mul-associates general_arith_equation1 primrec-unroll uiff_transitivity
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination lambdaFormation natural_numberEquality independent_isectElimination independent_functionElimination voidElimination sqequalRule lambdaEquality dependent_functionElimination isect_memberEquality sqequalAxiom because_Cache voidEquality unionElimination independent_pairFormation productElimination addEquality applyEquality intEquality minusEquality equalityTransitivity equalitySymmetry baseClosed equalityElimination dependent_pairFormation promote_hyp instantiate cumulativity impliesFunctionality multiplyEquality dependent_set_memberEquality imageMemberEquality baseApply closedConclusion

Latex:
\mforall{}[b,F:Top].  \mforall{}[n,m:\mBbbN{}].    (primrec(n  +  m;b;\mlambda{}i.F)  \msim{}  primrec(n;primrec(m;b;\mlambda{}i.F);\mlambda{}i.F))

Date html generated: 2017_04_14-AM-07_25_50
Last ObjectModification: 2017_02_27-PM-02_55_37

Theory : call!by!value_2

Home Index