---

Step * 1 1 of Lemma fps-compose-mul

.....assertion..... 
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∈⋃p∈bag-partitions(eq;b).bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)). ((g 
                                                                                    (hd(fst(p))
                                                                                    + bag-rep(||tl(fst(p))||;x))) 
                                                                                   * 
                                                                                   Πa ∈ tl(fst(p)). f a) 
                                                                                  * 
                                                                                  ((h 
                                                                                    (hd(snd(p))
                                                                                    + bag-rep(||tl(snd(p))||;x))) 
                                                                                   * 
                                                                                   Πa ∈ tl(snd(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|
BY
{ ((InstLemma `bag-summation-reindex` [⌜|r|⌝;⌜+r⌝;⌜0⌝;⌜Top × bag(X) List+ × bag(X) List+⌝;⌜bag(X) List+ × bag(X) List+⌝;
    ⌜λ2p.snd(p)⌝; ⌜λ2x.<⋅, x>⌝]⋅
    THENA Auto
    )
   THEN (RW (AddrC [3] (HypC (-1))) 0⋅ THEN Auto)
   THEN Try (Complete ((D -1 THEN Reduce 0 THEN EqCD THEN Auto)))) }

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)
17. ∀[f:(Top × bag(X) List+ × bag(X) List+) ⟶ |r|]
      ∀[b:bag(Top × bag(X) List+ × bag(X) List+)]. (Σ(x∈b). f[x] = Σ(x∈bag-map(λ2p.snd(p);b)). f[<⋅, x>] ∈ |r|) 
      supposing ∀x:Top × bag(X) List+ × bag(X) List+. (x = <⋅, snd(x)> ∈ (Top × bag(X) List+ × bag(X) List+))
⊢ Σ(p∈⋃p∈bag-partitions(eq;b).bag-parts'(eq;fst(p);x) × bag-parts'(eq;snd(p);x)). ((g 
                                                                                    (hd(fst(p))
                                                                                    + bag-rep(||tl(fst(p))||;x))) 
                                                                                   * 
                                                                                   Πa ∈ tl(fst(p)). f a) 
                                                                                  * 
                                                                                  ((h 
                                                                                    (hd(snd(p))
                                                                                    + bag-rep(||tl(snd(p))||;x))) 
                                                                                   * 
                                                                                   Πa ∈ tl(snd(p)). f a)
= Σ(p∈bag-map(λ2p.snd(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\000C(<⋅, p>))) + bag-rep(||tl(snd(snd(<⋅, p>)))||;x))) * Πa ∈ tl(snd(snd(<⋅, p>))). f a)
∈ |r|

---

Latex:

---

Latex:
.....assertion..... 
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.  \mforall{}L:bag(X)  List\msupplus{}.  (||L||  \mgeq{}  1  )
10.  Assoc(|r|;+r)
11.  IsMonoid(|r|;+r;0)
12.  Comm(|r|;+r)
13.  Comm(|r|;*)
14.  Assoc(|r|;*)
15.  \mforall{}L:bag(X)  List\msupplus{}.  (\mPi{}a  \mmember{}  tl(L).  f  a  \mmember{}  |r|)
16.  b  :  bag(X)
\mvdash{}  \mSigma{}(p\mmember{}\mcup{}p\mmember{}bag-partitions(eq;b).bag-parts'(eq;fst(p);x)  \mtimes{}  bag-parts'(eq;snd(p);x))
      ((g  (hd(fst(p))  +  bag-rep(||tl(fst(p))||;x)))  *  \mPi{}a  \mmember{}  tl(fst(p)).  f  a) 
      * 
      ((h  (hd(snd(p))  +  bag-rep(||tl(snd(p))||;x)))  *  \mPi{}a  \mmember{}  tl(snd(p)).  f  a)
=  \mSigma{}(p\mmember{}\mcup{}p\mmember{}bag-partitions(eq;b).
            bag-map(\mlambda{}p1.<p,  p1>bag-parts'(eq;fst(p);x)  \mtimes{}  bag-parts'(eq;snd(p);x)))
      ((g  (hd(fst(snd(p)))  +  bag-rep(||tl(fst(snd(p)))||;x)))  *  \mPi{}a  \mmember{}  tl(fst(snd(p))).  f  a) 
      * 
      ((h  (hd(snd(snd(p)))  +  bag-rep(||tl(snd(snd(p)))||;x)))  *  \mPi{}a  \mmember{}  tl(snd(snd(p))).  f  a)


By

---

Latex:
((InstLemma  `bag-summation-reindex`  [\mkleeneopen{}|r|\mkleeneclose{};\mkleeneopen{}+r\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}Top  \mtimes{}  bag(X)  List\msupplus{}  \mtimes{}  bag(X)  List\msupplus{}\mkleeneclose{};
    \mkleeneopen{}bag(X)  List\msupplus{}  \mtimes{}  bag(X)  List\msupplus{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}p.snd(p)\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}x.<\mcdot{},  x>\mkleeneclose{}]\mcdot{}
    THENA  Auto
    )
  THEN  (RW  (AddrC  [3]  (HypC  (-1)))  0\mcdot{}  THEN  Auto)
  THEN  Try  (Complete  ((D  -1  THEN  Reduce  0  THEN  EqCD  THEN  Auto))))

---

Home Index