### 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: `{}`
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