### Nuprl Lemma : fps-compose-single-general

[X:Type]
∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[b:bag(X)]. ∀[f:PowerSeries(X;r)].
(<b>(x:=f) (<(b|¬x)>*((f-(f[{}])*1))^(#((b|x)))) ∈ PowerSeries(X;r))
supposing valueall-type(X)

Proof

Definitions occuring in Statement :  fps-compose: g(x:=f) fps-exp: (f)^(n) fps-scalar-mul: (c)*f fps-mul: (f*g) fps-sub: (f-g) fps-single: <c> fps-one: 1 fps-coeff: f[b] power-series: PowerSeries(X;r) bag-co-restrict: (b|¬x) bag-restrict: (b|x) bag-size: #(bs) empty-bag: {} bag: bag(T) deq: EqDecider(T) valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] universe: Type equal: t ∈ T crng: CRng
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a true: True squash: T prop: subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q all: x:A. B[x]
Lemmas referenced :  bag-restrict-split power-series_wf bag_wf crng_wf deq_wf valueall-type_wf fps-mul_wf fps-single_wf bag-co-restrict_wf fps-exp_wf fps-sub_wf fps-scalar-mul_wf fps-coeff_wf empty-bag_wf fps-one_wf bag-size_wf bag-restrict_wf equal_wf squash_wf true_wf fps-compose_wf subtype_rel_self iff_weakening_equal fps-compose-mul fps-compose-single-disjoint bag-co-restrict-property bag-append-comm fps-mul-single bag-rep-size-restrict nat_wf fps-single-bag-rep fps-atom_wf fps-compose-exp fps-compose-atom-eq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality hypothesis sqequalRule isect_memberEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality natural_numberEquality independent_isectElimination applyEquality lambdaEquality imageElimination imageMemberEquality baseClosed instantiate productElimination independent_functionElimination lambdaFormation rename dependent_functionElimination hyp_replacement applyLambdaEquality

Latex:
\mforall{}[X:Type]
\mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x:X].  \mforall{}[b:bag(X)].  \mforall{}[f:PowerSeries(X;r)].
(<b>(x:=f)  =  (<(b|\mneg{}x)>*((f-(f[\{\}])*1))\^{}(\#((b|x)))))
supposing  valueall-type(X)

Date html generated: 2018_05_21-PM-10_10_20
Last ObjectModification: 2018_05_19-PM-04_15_10

Theory : power!series

Home Index