### Nuprl Lemma : fps-summation-coeff

`∀[X:Type]. ∀[r:CRng]. ∀[T:Type]. ∀[f:T ⟶ PowerSeries(X;r)]. ∀[b:bag(T)].`
`  ∀m:bag(X). (fps-summation(r;b;x.f[x])[m] = Σ(x∈b). f[x][m] ∈ |r|)`

Proof

Definitions occuring in Statement :  fps-summation: `fps-summation(r;b;x.f[x])` fps-coeff: `f[b]` power-series: `PowerSeries(X;r)` bag-summation: `Σ(x∈b). f[x]` bag: `bag(T)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T` crng: `CRng` rng_zero: `0` rng_plus: `+r` rng_car: `|r|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` squash: `↓T` exists: `∃x:A. B[x]` prop: `ℙ` crng: `CRng` rng: `Rng` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` and: `P ∧ Q` cand: `A c∧ B` fps-coeff: `f[b]` bag-summation: `Σ(x∈b). f[x]` fps-summation: `fps-summation(r;b;x.f[x])` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` fps-add: `(f+g)` fps-zero: `0` nat: `ℕ` implies: `P `` Q` false: `False` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` top: `Top` guard: `{T}` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` subtype_rel: `A ⊆r B` le: `A ≤ B` less_than': `less_than'(a;b)` less_than: `a < b` cons: `[a / b]` assert: `↑b` ifthenelse: `if b then t else f fi ` bfalse: `ff` iff: `P `⇐⇒` Q` uiff: `uiff(P;Q)` rev_implies: `P `` Q` int_iseg: `{i...j}` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` power-series: `PowerSeries(X;r)`
Lemmas referenced :  bag_to_squash_list equal_wf rng_car_wf fps-coeff_wf fps-summation_wf bag-summation_wf rng_plus_wf rng_zero_wf rng_all_properties rng_plus_comm2 bag_wf power-series_wf crng_wf nat_properties satisfiable-full-omega-tt intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma 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 less_than_wf le_wf length_wf int_seg_wf int_seg_properties decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma decidable__equal_int int_seg_subtype false_wf set_wf lelt_wf intformeq_wf int_formula_prop_eq_lemma non_neg_length decidable__lt decidable__assert null_wf3 subtype_rel_list top_wf list-cases product_subtype_list null_cons_lemma last-lemma-sq pos_length iff_transitivity not_wf equal-wf-T-base list_wf assert_wf bnot_wf assert_of_null iff_weakening_uiff assert_of_bnot firstn_wf length_firstn itermAdd_wf int_term_value_add_lemma nat_wf length_wf_nat list_accum_nil_lemma list_accum_cons_lemma last_wf list_accum_append
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality imageElimination productElimination promote_hyp hypothesis rename hyp_replacement equalitySymmetry Error :applyLambdaEquality,  setElimination because_Cache cumulativity sqequalRule lambdaEquality applyEquality functionExtensionality independent_isectElimination independent_pairFormation dependent_functionElimination axiomEquality isect_memberEquality functionEquality universeEquality intWeakElimination natural_numberEquality dependent_pairFormation int_eqEquality intEquality voidElimination voidEquality computeAll independent_functionElimination unionElimination equalityTransitivity hypothesis_subsumption dependent_set_memberEquality baseClosed impliesFunctionality productEquality addEquality

Latex:
\mforall{}[X:Type].  \mforall{}[r:CRng].  \mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  PowerSeries(X;r)].  \mforall{}[b:bag(T)].
\mforall{}m:bag(X).  (fps-summation(r;b;x.f[x])[m]  =  \mSigma{}(x\mmember{}b).  f[x][m])

Date html generated: 2016_10_25-AM-11_34_15
Last ObjectModification: 2016_07_12-AM-07_37_52

Theory : power!series

Home Index