### Nuprl Lemma : fps-compose-single

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

Proof

Definitions occuring in Statement :  fps-compose: `g(x:=f)` fps-exp: `(f)^(n)` fps-mul: `(f*g)` fps-single: `<c>` 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: `b supposing a` uall: `∀[x:A]. B[x]` universe: `Type` equal: `s = t ∈ T` crng: `CRng` rng_zero: `0` rng_car: `|r|`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` squash: `↓T` prop: `ℙ` true: `True` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` crng: `CRng` rng: `Rng` fps-sub: `(f-g)`
Lemmas referenced :  equal_wf squash_wf true_wf fps-compose-single-general fps-mul_wf fps-single_wf bag-co-restrict_wf fps-exp_wf bag-size_wf bag-restrict_wf subtype_rel_self iff_weakening_equal valueall-type_wf power-series_wf crng_wf deq_wf rng_car_wf fps-coeff_wf empty-bag_wf rng_zero_wf bag_wf fps-one_wf fps-scalar-mul-zero fps-sub_wf fps-scalar-mul_wf neg_id_fps mon_ident_fps fps-add_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut applyEquality thin lambdaEquality sqequalHypSubstitution imageElimination extract_by_obid isectElimination hypothesisEquality equalityTransitivity hypothesis equalitySymmetry because_Cache independent_isectElimination natural_numberEquality sqequalRule imageMemberEquality baseClosed instantiate productElimination independent_functionElimination setElimination rename isect_memberEquality axiomEquality universeEquality 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)\^{}(\#((b|x))))  supposing  f[\{\}]  =  0
supposing  valueall-type(X)

Date html generated: 2018_05_21-PM-10_10_24
Last ObjectModification: 2018_05_19-PM-04_15_20

Theory : power!series

Home Index