---

Step * 1 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∈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|
BY
{ ((Assert ⋃x∈bag-partitions(eq;b).bag-map(λy.<fst(x), y>;bag-partitions(eq;snd(x)))
          = 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;fst(p))))
          ∈ bag(bag(X) × bag(X) × bag(X)) BY
          Auto)
THENM ((HypSubst' -1 0 THENA Auto)
       THEN GenConclAtAddrType ⌜bag(bag(X) × bag(X) × bag(X))⌝ [2;3]⋅
       THEN Auto
       THEN EqCD
       THEN Auto)
) }

---

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{}bag-map(\mlambda{}\msubtwo{}p.<fst(snd(p)),  snd(snd(p)),  fst(p)>
            \mcup{}p\mmember{}bag-partitions(eq;b).bag-map(\mlambda{}p1.<snd(p),  p1>bag-partitions(eq;fst(p)))))
      (f[fst(p)]  *  g[fst(snd(p))])  *  h[snd(snd(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:
((Assert  \mcup{}x\mmember{}bag-partitions(eq;b).bag-map(\mlambda{}y.<fst(x),  y>bag-partitions(eq;snd(x)))
                =  bag-map(\mlambda{}\msubtwo{}p.<fst(snd(p)),  snd(snd(p)),  fst(p)>
                    \mcup{}p\mmember{}bag-partitions(eq;b).bag-map(\mlambda{}p1.<snd(p),  p1>bag-partitions(eq;fst(p))))  BY
                Auto)
THENM  ((HypSubst'  -1  0  THENA  Auto)
              THEN  GenConclAtAddrType  \mkleeneopen{}bag(bag(X)  \mtimes{}  bag(X)  \mtimes{}  bag(X))\mkleeneclose{}  [2;3]\mcdot{}
              THEN  Auto
              THEN  EqCD
              THEN  Auto)
)

---

Home Index