---

Step * 1 1 of Lemma fps-mul-assoc


1. X : Type
2. eq : EqDecider(X)
3. valueall-type(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. g : PowerSeries(X;r)
7. h : PowerSeries(X;r)
8. Assoc(|r|;+r)
9. Comm(|r|;+r)
10. BiLinear(|r|;+r;*)
11. Assoc(|r|;*)
12. b : bag(X)@i
13. minus : |r| ⟶ |r|
14. IsMonoid(|r|;+r;0)
15. Inverse(|r|;+r;0;minus)
⊢ Σ(p∈⋃p∈bag-partitions(eq;b).bag-map(λp1.<snd(p), p1>;bag-partitions(eq;fst(p)))). (f[fst(snd(p))] * g[snd(snd(p))]) 
                                                                                    * 
                                                                                    h[fst(p)]
= Σ(p∈⋃x∈bag-partitions(eq;b).bag-map(λy.<fst(x), y>;bag-partitions(eq;snd(x)))). f[fst(p)] 
                                                                                  * 
                                                                                  (g[fst(snd(p))] * h[snd(snd(p))])
∈ |r|
BY
{ TACTIC:((InstLemma `bag-summation-map` [⌜+r⌝;⌜0⌝;
           ⌜⋃p∈bag-partitions(eq;b).bag-map(λp1.<snd(p), p1>;bag-partitions(eq;fst(p)))⌝;⌜λ2p.(f[fst(p)] 
                                                                                               * 
                                                                                               g[fst(snd(p))]) 
                                                                                              * 
                                                                                              h[snd(snd(p))]⌝;
           ⌜λ2p.<fst(snd(p)), snd(snd(p)), fst(p)>⌝]⋅
           THENA (Auto THEN SubsumeC ⌜bag(bag(X) × bag(X) × bag(X))⌝⋅ THEN Auto)
           )
          THEN Reduce (-1)
          THEN RevHypSubst' (-1) 0
          THEN Thin (-1))⋅ }

1
1. X : Type
2. eq : EqDecider(X)
3. valueall-type(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. g : PowerSeries(X;r)
7. h : PowerSeries(X;r)
8. Assoc(|r|;+r)
9. Comm(|r|;+r)
10. BiLinear(|r|;+r;*)
11. Assoc(|r|;*)
12. b : bag(X)@i
13. minus : |r| ⟶ |r|
14. IsMonoid(|r|;+r;0)
15. Inverse(|r|;+r;0;minus)
⊢ Σ(p∈bag-map(λ2p.<fst(snd(p)), snd(snd(p)), fst(p)>;⋃p∈bag-partitions(eq;b).bag-map(λp1.<snd(p), p1>;bag-partitions(eq;\000Cfst(p)))))
   (f[fst(p)] * g[fst(snd(p))]) * h[snd(snd(p))]
= Σ(p∈⋃x∈bag-partitions(eq;b).bag-map(λy.<fst(x), y>;bag-partitions(eq;snd(x)))). f[fst(p)] 
                                                                                  * 
                                                                                  (g[fst(snd(p))] * h[snd(snd(p))])
∈ |r|

---

Latex:

---

Latex:

1.  X  :  Type
2.  eq  :  EqDecider(X)
3.  valueall-type(X)
4.  r  :  CRng
5.  f  :  PowerSeries(X;r)
6.  g  :  PowerSeries(X;r)
7.  h  :  PowerSeries(X;r)
8.  Assoc(|r|;+r)
9.  Comm(|r|;+r)
10.  BiLinear(|r|;+r;*)
11.  Assoc(|r|;*)
12.  b  :  bag(X)@i
13.  minus  :  |r|  {}\mrightarrow{}  |r|
14.  IsMonoid(|r|;+r;0)
15.  Inverse(|r|;+r;0;minus)
\mvdash{}  \mSigma{}(p\mmember{}\mcup{}p\mmember{}bag-partitions(eq;b).bag-map(\mlambda{}p1.<snd(p),  p1>bag-partitions(eq;fst(p))))
      (f[fst(snd(p))]  *  g[snd(snd(p))])  *  h[fst(p)]
=  \mSigma{}(p\mmember{}\mcup{}x\mmember{}bag-partitions(eq;b).bag-map(\mlambda{}y.<fst(x),  y>bag-partitions(eq;snd(x)))).  f[fst(p)] 
                                                                                                                                                                    * 
                                                                                                                                                                    (g[fst(snd(p))] 
                                                                                                                                                                      * 
                                                                                                                                                                      h[snd(snd(p))])


By

---

Latex:
TACTIC:((InstLemma  `bag-summation-map`  [\mkleeneopen{}+r\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};
                  \mkleeneopen{}\mcup{}p\mmember{}bag-partitions(eq;b).bag-map(\mlambda{}p1.<snd(p),  p1>bag-partitions(eq;fst(p)))\mkleeneclose{};
                  \mkleeneopen{}\mlambda{}\msubtwo{}p.(f[fst(p)]  *  g[fst(snd(p))])  *  h[snd(snd(p))]\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.<fst(snd(p)),  snd(snd(p)),  fst(p)>\000C\mkleeneclose{}]\mcdot{}
                  THENA  (Auto  THEN  SubsumeC  \mkleeneopen{}bag(bag(X)  \mtimes{}  bag(X)  \mtimes{}  bag(X))\mkleeneclose{}\mcdot{}  THEN  Auto)
                  )
                THEN  Reduce  (-1)
                THEN  RevHypSubst'  (-1)  0
                THEN  Thin  (-1))\mcdot{}

---

Home Index