---

Definition: fps-alg
fps-alg(X;eq;r) ==  <PowerSeries(X;r), λf,g. tt, λf,g. tt, λf,g. (f+g), 0, λf.-(f), λf,g. (f*g), 1, λf,g. (inl f), λc,f.\000C (c)*f>

Lemma: fps-alg_wf
∀[X:Type]. ∀[eq:EqDecider(X)].  ∀[r:CRng]. (fps-alg(X;eq;r) ∈ CAlg(r)) supposing valueall-type(X)



Home Index