### Nuprl Lemma : sum-unroll

`∀[n,f:Top].  (Σ(f[x] | x < n) ~ if (0) < (n)  then Σ(f[x] | x < n - 1) + f[n - 1]  else 0)`

Proof

Definitions occuring in Statement :  sum: `Σ(f[x] | x < k)` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` less: `if (a) < (b)  then c  else d` subtract: `n - m` add: `n + m` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` implies: `P `` Q` all: `∀x:A. B[x]` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` less_than: `a < b` less_than': `less_than'(a;b)` top: `Top` true: `True` squash: `↓T` not: `¬A` false: `False` bfalse: `ff` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b` rev_implies: `P `` Q` iff: `P `⇐⇒` Q` prop: `ℙ` nat: `ℕ` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` ge: `i ≥ j ` sum: `Σ(f[x] | x < k)` sum_aux: `sum_aux(k;v;i;x.f[x])` has-value: `(a)↓` so_apply: `x[s]` so_lambda: `λ2x.t[x]`
Lemmas referenced :  top_wf lt_int_wf eqtt_to_assert assert_of_lt_int istype-void eqff_to_assert bool_subtype_base bool_cases_sqequal subtype_base_sq bool_wf assert-bnot iff_weakening_uiff assert_wf less_than_wf decidable__le subtract_wf full-omega-unsat intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf int_subtype_base nat_properties decidable__equal_int intformeq_wf itermAdd_wf int_formula_prop_eq_lemma int_term_value_add_lemma ge_wf subtract-1-ge-0 decidable__lt value-type-has-value int-value-type less_than_anti-reflexive add-zero add-commutes exception-not-value has-value_wf_base is-exception_wf subtract-add-cancel base_wf subtype_rel_self zero-add sum-has-value equal_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity Error :isect_memberFormation_alt,  introduction cut sqequalRule thin sqequalHypSubstitution hypothesis axiomSqEquality Error :inhabitedIsType,  hypothesisEquality Error :isect_memberEquality_alt,  isectElimination Error :isectIsTypeImplies,  Error :universeIsType,  extract_by_obid Error :lambdaFormation_alt,  natural_numberEquality unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination lessCases independent_pairFormation voidElimination imageMemberEquality baseClosed imageElimination independent_functionElimination Error :dependent_pairFormation_alt,  Error :equalityIsType4,  baseApply closedConclusion applyEquality promote_hyp dependent_functionElimination instantiate cumulativity because_Cache Error :equalityIsType1,  intEquality Error :dependent_set_memberEquality_alt,  approximateComputation Error :lambdaEquality_alt,  int_eqEquality applyLambdaEquality setElimination rename intWeakElimination Error :functionIsTypeImplies,  addEquality callbyvalueReduce sqequalSqle divergentSqle callbyvalueCallbyvalue sqleReflexivity callbyvalueExceptionCases axiomSqleEquality addExceptionCases exceptionSqequal callbyvalueAdd lessExceptionCases dependent_pairFormation voidEquality isect_memberEquality isect_memberFormation lambdaFormation callbyvalueLess

Latex:
\mforall{}[n,f:Top].    (\mSigma{}(f[x]  |  x  <  n)  \msim{}  if  (0)  <  (n)    then  \mSigma{}(f[x]  |  x  <  n  -  1)  +  f[n  -  1]    else  0)

Date html generated: 2019_06_20-PM-01_18_01
Last ObjectModification: 2018_10_15-PM-01_51_02

Theory : int_2

Home Index