### Nuprl Lemma : bag-summation-from-upto

`∀[a,b:ℤ]. ∀[f:{a..b-} ⟶ ℤ].  (Σ(i∈[a, b)). f[i] = Σ(f[j + a] | j < b - a) ∈ ℤ)`

Proof

Definitions occuring in Statement :  bag-summation: `Σ(x∈b). f[x]` from-upto: `[n, m)` sum: `Σ(f[x] | x < k)` int_seg: `{i..j-}` uall: `∀[x:A]. B[x]` so_apply: `x[s]` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` subtract: `n - m` add: `n + m` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` uimplies: `b supposing a` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` and: `P ∧ Q` prop: `ℙ` nil: `[]` list_accum: list_accum bag-accum: `bag-accum(v,x.f[v; x];init;bs)` bag-summation: `Σ(x∈b). f[x]` squash: `↓T` true: `True` less_than': `less_than'(a;b)` less_than: `a < b` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` assert: `↑b` bnot: `¬bb` guard: `{T}` sq_type: `SQType(T)` or: `P ∨ Q` subtype_rel: `A ⊆r B` bfalse: `ff` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` btrue: `tt` it: `⋅` unit: `Unit` bool: `𝔹` from-upto: `[n, m)` sum_aux: `sum_aux(k;v;i;x.f[x])` sum: `Σ(f[x] | x < k)` decidable: `Dec(P)` nat_plus: `ℕ+` so_lambda: `λ2x.t[x]` so_apply: `x[s]` int_seg: `{i..j-}` lelt: `i ≤ j < k` subtract: `n - m` bag-append: `as + bs` cand: `A c∧ B` monoid_p: `IsMonoid(T;op;id)` assoc: `Assoc(T;op)` infix_ap: `x f y` ident: `Ident(T;op;id)` comm: `Comm(T;op)` le: `A ≤ B` bag-map: `bag-map(f;bs)` has-value: `(a)↓` single-bag: `{x}` cons: `[a / b]` empty-bag: `{}`
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than int_seg_wf subtract_wf subtract-1-ge-0 istype-nat istype-top less_than_wf assert_wf iff_weakening_uiff assert-bnot bool_subtype_base bool_wf subtype_base_sq bool_cases_sqequal int_subtype_base eqff_to_assert int_term_value_subtract_lemma itermSubtract_wf assert_of_lt_int eqtt_to_assert lt_int_wf decidable__lt sum_split1 intformnot_wf int_formula_prop_not_lemma add-member-int_seg2 decidable__le istype-le general_arith_equation2 itermAdd_wf int_term_value_add_lemma decidable__equal_int intformeq_wf int_formula_prop_eq_lemma int_seg_properties add-member-int_seg1 zero-add add-commutes add-swap add-associates le_wf sum_wf from-upto-split bag-summation-append equal_wf squash_wf true_wf istype-universe from-upto_wf list-subtype-bag subtype_rel_sets_simple lelt_wf istype-false not-lt-2 less-iff-le condition-implies-le minus-add minus-one-mul minus-one-mul-top add_functionality_wrt_le le-add-cancel2 not-le-2 minus-minus le-add-cancel subtype_rel_self iff_weakening_equal bag-summation_wf from-upto-shift subtract-add-cancel top_wf subtype_rel_list bag-summation-map subtype_rel_sets add-subtract-cancel bag_wf comm_wf assoc_wf value-type-has-value int-value-type list_wf list_subtype_base cons_wf nil_wf bag-summation-single bag-summation-empty satisfiable-full-omega-tt
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation_alt introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation_alt lambdaEquality_alt int_eqEquality dependent_functionElimination isect_memberEquality_alt voidElimination sqequalRule independent_pairFormation universeIsType axiomEquality isectIsTypeImplies inhabitedIsType functionIsTypeImplies isect_memberFormation_alt functionIsType because_Cache equalityIsType1 imageElimination imageMemberEquality axiomSqEquality lessCases cumulativity instantiate promote_hyp applyEquality baseClosed closedConclusion baseApply equalityIsType2 sqleReflexivity callbyvalueReduce productElimination equalitySymmetry equalityTransitivity equalityElimination unionElimination intEquality dependent_set_memberEquality_alt productIsType addEquality independent_pairEquality universeEquality setEquality productEquality minusEquality setIsType equalityIstype isect_memberFormation functionEquality isect_memberEquality dependent_set_memberEquality dependent_pairFormation lambdaEquality voidEquality computeAll functionExtensionality lambdaFormation

Latex:
\mforall{}[a,b:\mBbbZ{}].  \mforall{}[f:\{a..b\msupminus{}\}  {}\mrightarrow{}  \mBbbZ{}].    (\mSigma{}(i\mmember{}[a,  b)).  f[i]  =  \mSigma{}(f[j  +  a]  |  j  <  b  -  a))

Date html generated: 2019_10_15-AM-11_03_47
Last ObjectModification: 2018_11_27-AM-00_30_14

Theory : bags

Home Index