---

Step * of Lemma fps-compose-ucont

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[g:PowerSeries(X;r)].  ∀x:X. fps-ucont(X;eq;r;f.f(x:=g)) supposing valueall-type(X)
BY
{ (((Auto
     THEN (Assert Comm(|r|;+r) ∧ IsMonoid(|r|;+r;0) ∧ Assoc(|r|;*) ∧ Comm(|r|;*) BY
                 ((InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENA Auto)
                  THEN Fold `comm` (-1)
                  THEN Auto
                  THEN Unhide
                  THEN Auto
                  THEN RepeatFor 2 (DVar `r')⋅
                  THEN Auto))
     )
    THEN D 0
    THEN Auto)
   THEN With ⌜b + bag-rep(#(b);x)⌝ (D 0)⋅
   THEN Auto
   THEN RepUR ``fps-coeff fps-compose fps-restrict`` 0
   THEN Folds ``hdp tlp`` 0
   THEN BLemma `bag-summation-equal`
   THEN Auto
   THEN AutoSplit
   THEN D (-2)) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. g : PowerSeries(X;r)
6. x : X
7. Comm(|r|;+r)
8. IsMonoid(|r|;+r;0)
9. Assoc(|r|;*)
10. Comm(|r|;*)
11. b : bag(X)
12. f : PowerSeries(X;r)
13. L : bag(X) List+
14. L ↓∈ bag-parts'(eq;b;x)
⊢ sub-bag(X;hdp(L) + bag-rep(||tlp(L)||;x);b + bag-rep(#(b);x))

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[g:PowerSeries(X;r)].    \mforall{}x:X.  fps-ucont(X;eq;r;f.f(x:=g)) 
    supposing  valueall-type(X)


By

---

Latex:
(((Auto
      THEN  (Assert  Comm(|r|;+r)  \mwedge{}  IsMonoid(|r|;+r;0)  \mwedge{}  Assoc(|r|;*)  \mwedge{}  Comm(|r|;*)  BY
                              ((InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                THEN  Fold  `comm`  (-1)
                                THEN  Auto
                                THEN  Unhide
                                THEN  Auto
                                THEN  RepeatFor  2  (DVar  `r')\mcdot{}
                                THEN  Auto))
      )
    THEN  D  0
    THEN  Auto)
  THEN  With  \mkleeneopen{}b  +  bag-rep(\#(b);x)\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto
  THEN  RepUR  ``fps-coeff  fps-compose  fps-restrict``  0
  THEN  Folds  ``hdp  tlp``  0
  THEN  BLemma  `bag-summation-equal`
  THEN  Auto
  THEN  AutoSplit
  THEN  D  (-2))

---

Home Index