Nuprl Lemma : fps-restrict-summation

`∀[X:Type]`
`  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[f:PowerSeries(X;r)]. ∀[d:bag(X)].`
`    (fps-restrict(eq;r;f;d) = Σ(x∈sub-bags(eq;d)). (f[x])*<x> ∈ PowerSeries(X;r)) `
`  supposing valueall-type(X)`

Proof

Definitions occuring in Statement :  fps-restrict: `fps-restrict(eq;r;f;d)` fps-scalar-mul: `(c)*f` fps-add: `(f+g)` fps-single: `<c>` fps-zero: `0` fps-coeff: `f[b]` power-series: `PowerSeries(X;r)` sub-bags: `sub-bags(eq;bs)` bag-summation: `Σ(x∈b). f[x]` bag: `bag(T)` deq: `EqDecider(T)` valueall-type: `valueall-type(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` lambda: `λx.A[x]` universe: `Type` equal: `s = t ∈ T` crng: `CRng`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` cand: `A c∧ B` assoc: `Assoc(T;op)` infix_ap: `x f y` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` implies: `P `` Q` comm: `Comm(T;op)` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uiff: `uiff(P;Q)` all: `∀x:A. B[x]` fps-single: `<c>` fps-coeff: `f[b]` fps-scalar-mul: `(c)*f` fps-restrict: `fps-restrict(eq;r;f;d)` crng: `CRng` rng: `Rng` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` ifthenelse: `if b then t else f fi ` power-series: `PowerSeries(X;r)` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` ring_p: `IsRing(T;plus;zero;neg;times;one)` group_p: `IsGroup(T;op;id;inv)` bag-member: `x ↓∈ bs` rev_uimplies: `rev_uimplies(P;Q)` top: `Top` bag-summation: `Σ(x∈b). f[x]` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` list_accum: list_accum nil: `[]` fps-zero: `0` rng_zero: `0` pi1: `fst(t)` pi2: `snd(t)` cons-bag: `x.b` monoid_p: `IsMonoid(T;op;id)` ident: `Ident(T;op;id)` fps-add: `(f+g)`
Lemmas referenced :  equal_wf squash_wf true_wf power-series_wf mon_assoc_fps fps-add_wf iff_weakening_equal fps-add-comm fps-ext fps-restrict_wf bag-summation_wf bag_wf fps-zero_wf fps-scalar-mul_wf fps-coeff_wf fps-single_wf sub-bags_wf crng_wf deq_wf valueall-type_wf rng_car_wf deq-sub-bag_wf bool_wf eqtt_to_assert assert-deq-sub-bag eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot sub-bag_wf rng_zero_wf bag-summation-filter rng_plus_wf bag-eq_wf rng_plus_comm2 crng_properties rng_properties rng_all_properties bag-extensionality-no-repeats decidable__equal_bag decidable-equal-deq bag-filter_wf subtype_rel_bag assert_wf single-bag_wf bag-filter-no-repeats sub-bags-no-repeats bag-single-no-repeats bag-member-single bag-member-filter assert-bag-eq bag-member_wf member-sub-bags and_wf bag-summation-single bag-summation-empty equal-empty-bag empty-bag-iff-no-member set_wf bag-member-filter-set rng_times_one rng_times_zero bag_to_squash_list list_induction list-subtype-bag subtype_rel_self list_wf nil_wf cons-bag-as-append bag-summation-append abmonoid_comm_fps mon_ident_fps isect_subtype_rel_trivial subtype_rel_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache cumulativity natural_numberEquality imageMemberEquality baseClosed universeEquality independent_isectElimination productElimination independent_functionElimination isect_memberEquality axiomEquality independent_pairFormation lambdaFormation setElimination rename unionElimination equalityElimination dependent_functionElimination dependent_pairFormation promote_hyp instantiate voidElimination hyp_replacement applyLambdaEquality setEquality dependent_set_memberEquality addLevel productEquality voidEquality equalityUniverse levelHypothesis independent_pairEquality functionEquality functionExtensionality

Latex:
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[f:PowerSeries(X;r)].  \mforall{}[d:bag(X)].
(fps-restrict(eq;r;f;d)  =  \mSigma{}(x\mmember{}sub-bags(eq;d)).  (f[x])*<x>)
supposing  valueall-type(X)

Date html generated: 2018_05_21-PM-10_10_37
Last ObjectModification: 2017_07_26-PM-06_34_24

Theory : power!series

Home Index