---

Step * 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|. IsGroup(|r|;+r;0;minus)
⊢ Σ(p∈bag-partitions(eq;b)). Σ(p1∈bag-partitions(eq;fst(p))). (f[fst(p1)] * g[snd(p1)]) * h[snd(p)]
= Σ(p∈bag-partitions(eq;b)). Σ(p1∈bag-partitions(eq;snd(p))). f[fst(p)] * (g[fst(p1)] * h[snd(p1)])
∈ |r|
BY
{ ((ExRepD THEN D -1)
   THEN (InstLemma `bag-double-summation` [⌜|r|⌝;⌜+r⌝;⌜0⌝;⌜bag(X) × bag(X)⌝;⌜bag(X) × bag(X)⌝;⌜bag(X)⌝;
         ⌜λ2p.bag-partitions(eq;fst(p))⌝;⌜λ2p.snd(p)⌝;⌜λ2x p1.(f[fst(p1)] * g[snd(p1)]) * h[x]⌝]⋅
         THENA Auto
         )
   THEN RWO "-1" 0
   THEN Auto
   THEN Thin (-1)
   THEN ((InstLemma `bag-double-summation` [⌜|r|⌝;⌜+r⌝;⌜0⌝;⌜bag(X) × bag(X)⌝;⌜bag(X) × bag(X)⌝;⌜bag(X)⌝;
          ⌜λ2p.bag-partitions(eq;snd(p))⌝;⌜λ2p.fst(p)⌝;⌜λ2x p1.f[x] * (g[fst(p1)] * h[snd(p1)])⌝;⌜bag-partitions(eq;b)⌝]
          ⋅
          THENA Auto
          )
         THEN Symmetry
         THEN NthHypEq (-1)
         THEN EqCD
         THEN Auto
         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∈⋃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|

---

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.  \mexists{}minus:|r|  {}\mrightarrow{}  |r|.  IsGroup(|r|;+r;0;minus)
\mvdash{}  \mSigma{}(p\mmember{}bag-partitions(eq;b)).  \mSigma{}(p1\mmember{}bag-partitions(eq;fst(p))).  (f[fst(p1)]  *  g[snd(p1)])  *  h[snd(p)]
=  \mSigma{}(p\mmember{}bag-partitions(eq;b)).  \mSigma{}(p1\mmember{}bag-partitions(eq;snd(p))).  f[fst(p)]  *  (g[fst(p1)]  *  h[snd(p1)])


By

---

Latex:
((ExRepD  THEN  D  -1)
  THEN  (InstLemma  `bag-double-summation`  [\mkleeneopen{}|r|\mkleeneclose{};\mkleeneopen{}+r\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}bag(X)  \mtimes{}  bag(X)\mkleeneclose{};\mkleeneopen{}bag(X)  \mtimes{}  bag(X)\mkleeneclose{};\mkleeneopen{}bag(X)\mkleeneclose{}
              ;\mkleeneopen{}\mlambda{}\msubtwo{}p.bag-partitions(eq;fst(p))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.snd(p)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  p1.(f[fst(p1)]  *  g[snd(p1)])  *  h[x]\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  Thin  (-1)
  THEN  ((InstLemma  `bag-double-summation`  [\mkleeneopen{}|r|\mkleeneclose{};\mkleeneopen{}+r\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}bag(X)  \mtimes{}  bag(X)\mkleeneclose{};\mkleeneopen{}bag(X)  \mtimes{}  bag(X)\mkleeneclose{};
                \mkleeneopen{}bag(X)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.bag-partitions(eq;snd(p))\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.fst(p)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  p1.f[x] 
                                                                                                                                            * 
                                                                                                                                            (g[fst(p1)]  *  h[snd(p1)])\mkleeneclose{};
                \mkleeneopen{}bag-partitions(eq;b)\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )
              THEN  Symmetry
              THEN  NthHypEq  (-1)
              THEN  EqCD
              THEN  Auto
              THEN  Thin  (-1))\mcdot{})\mcdot{}

---

Home Index