---

Step * of Lemma fps-compose-mul

No Annotations
∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng]. ∀[x:X]. ∀[g,f,h:PowerSeries(X;r)].
    ((g*h)(x:=f) = (g(x:=f)*h(x:=f)) ∈ PowerSeries(X;r)) 
  supposing valueall-type(X)
BY
{ (Auto
   THEN (Assert (∀L:bag(X) List+. (||L|| ≥ 1 ))
               ∧ (Assoc(|r|;+r) ∧ IsMonoid(|r|;+r;0))
               ∧ (Comm(|r|;+r) ∧ Comm(|r|;*) ∧ Assoc(|r|;*))
               ∧ (∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)) BY
               ((InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENA Auto)
                THEN Fold `comm` (-1)
                THEN Auto
                THEN Try ((D -1 THEN Complete (Auto)))
                THEN Try ((Using [`T',⌜bag(X)⌝] MemCD⋅ THEN Auto))
                THEN RepeatFor 2 (DVar `r')
                THEN Auto
                THEN Auto))
   THEN TACTIC:(Auto
                THEN BLemma `fps-ext`
                THEN Auto
                THEN (RepUR ``fps-mul fps-compose fps-coeff`` 0
                      THEN (InstLemma `bag-summation-product` [⌜r⌝;⌜bag(X) List+⌝;⌜bag(X) List+⌝]⋅ THENA Auto)
                      THEN RWO "-1" 0
                      THEN Auto
                      THEN (InstLemma `bag-double-summation2` 
                            [⌜|r|⌝;⌜+r⌝;⌜0⌝;⌜bag(X) × bag(X)⌝;⌜bag(X) List+ × bag(X) List+⌝]⋅
                            THENA Auto
                            )⋅
                      THEN RWO "-1" 0
                      THEN Auto)
                THEN (RWO "bag-summation-ring-linear1.1<" 0 THENM RWO "bag-double-summation2" 0)
                THEN Auto
                THEN Try (Complete ((RepeatFor 2 (DVar `r') THEN Auto)⋅))
                THEN RepeatFor 2 (Thin (-1)))) }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. g : PowerSeries(X;r)
7. f : PowerSeries(X;r)
8. h : PowerSeries(X;r)
9. ∀L:bag(X) List+. (||L|| ≥ 1 )
10. Assoc(|r|;+r)
11. IsMonoid(|r|;+r;0)
12. Comm(|r|;+r)
13. Comm(|r|;*)
14. Assoc(|r|;*)
15. ∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)
16. b : bag(X)
⊢ Σ(p∈⋃L∈bag-parts'(eq;b;x).bag-map(λp.<L, p>;bag-partitions(eq;hd(L) + bag-rep(||tl(L)||;x)))). (* (g (fst(snd(p)))) 
                                                                                                  (h (snd(snd(p))))) 
                                                                                                 * 
                                                                                                 Πa ∈ tl(fst(p)). f a
= Σ(p∈⋃p∈bag-partitions(eq;b).bag-map(λp1.<p, p1>;bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)))
   ((g (hd(fst(snd(p))) + bag-rep(||tl(fst(snd(p)))||;x))) * Πa ∈ tl(fst(snd(p))). f a) 
   * 
   ((h (hd(snd(snd(p))) + bag-rep(||tl(snd(snd(p)))||;x))) * Πa ∈ tl(snd(snd(p))). f a)
∈ |r|

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].  \mforall{}[x:X].  \mforall{}[g,f,h:PowerSeries(X;r)].
        ((g*h)(x:=f)  =  (g(x:=f)*h(x:=f))) 
    supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  (Assert  (\mforall{}L:bag(X)  List\msupplus{}.  (||L||  \mgeq{}  1  ))
                          \mwedge{}  (Assoc(|r|;+r)  \mwedge{}  IsMonoid(|r|;+r;0))
                          \mwedge{}  (Comm(|r|;+r)  \mwedge{}  Comm(|r|;*)  \mwedge{}  Assoc(|r|;*))
                          \mwedge{}  (\mforall{}L:bag(X)  List\msupplus{}.  (\mPi{}a  \mmember{}  tl(L).  f  a  \mmember{}  |r|))  BY
                          ((InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  Fold  `comm`  (-1)
                            THEN  Auto
                            THEN  Try  ((D  -1  THEN  Complete  (Auto)))
                            THEN  Try  ((Using  [`T',\mkleeneopen{}bag(X)\mkleeneclose{}]  MemCD\mcdot{}  THEN  Auto))
                            THEN  RepeatFor  2  (DVar  `r')
                            THEN  Auto
                            THEN  Auto))
  THEN  TACTIC:(Auto
                            THEN  BLemma  `fps-ext`
                            THEN  Auto
                            THEN  (RepUR  ``fps-mul  fps-compose  fps-coeff``  0
                                        THEN  (InstLemma  `bag-summation-product`  [\mkleeneopen{}r\mkleeneclose{};\mkleeneopen{}bag(X)  List\msupplus{}\mkleeneclose{};\mkleeneopen{}bag(X)  List\msupplus{}\mkleeneclose{}]\mcdot{}
                                                    THENA  Auto
                                                    )
                                        THEN  RWO  "-1"  0
                                        THEN  Auto
                                        THEN  (InstLemma  `bag-double-summation2` 
                                                    [\mkleeneopen{}|r|\mkleeneclose{};\mkleeneopen{}+r\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}bag(X)  \mtimes{}  bag(X)\mkleeneclose{};\mkleeneopen{}bag(X)  List\msupplus{}  \mtimes{}  bag(X)  List\msupplus{}\mkleeneclose{}]\mcdot{}
                                                    THENA  Auto
                                                    )\mcdot{}
                                        THEN  RWO  "-1"  0
                                        THEN  Auto)
                            THEN  (RWO  "bag-summation-ring-linear1.1<"  0  THENM  RWO  "bag-double-summation2"  0)
                            THEN  Auto
                            THEN  Try  (Complete  ((RepeatFor  2  (DVar  `r')  THEN  Auto)\mcdot{}))
                            THEN  RepeatFor  2  (Thin  (-1))))

---

Home Index