---

Step * 1 1 1 2 1 1 1 of Lemma bag-summation-add


1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. zero : R
5. f : T ⟶ R
6. g : T ⟶ R
7. IsMonoid(R;add;zero)
8. Comm(R;add)
9. u : T
10. v : T List
11. ∀x,y,z:R.
      ((z = add[x;y] ∈ R)
      ⇒ (accumulate (with value c and list item x):
           add add[f[x];g[x]] c
          over list:
            v
          with starting value:
           z)
         = add[accumulate (with value c and list item x):
                add f[x] c
               over list:
                 v
               with starting value:
                x);accumulate (with value c and list item x):
                    add g[x] c
                   over list:
                     v
                   with starting value:
                    y)]
         ∈ R))
12. x : R
13. y : R
14. z : R
15. z = add[x;y] ∈ R
⊢ (((f u) add (g u)) add (x add y)) = (((f u) add x) add ((g u) add y)) ∈ R
BY
{ (D 7
   THEN Unfold `assoc` 7
   THEN (RWO "7" 0 THEN Auto THEN EqCD THEN Auto)
   THEN RWO "7<" 0
   THEN Auto
   THEN EqCD
   THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  Type
3.  add  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
4.  zero  :  R
5.  f  :  T  {}\mrightarrow{}  R
6.  g  :  T  {}\mrightarrow{}  R
7.  IsMonoid(R;add;zero)
8.  Comm(R;add)
9.  u  :  T
10.  v  :  T  List
11.  \mforall{}x,y,z:R.
            ((z  =  add[x;y])
            {}\mRightarrow{}  (accumulate  (with  value  c  and  list  item  x):
                      add  add[f[x];g[x]]  c
                    over  list:
                        v
                    with  starting  value:
                      z)
                  =  add[accumulate  (with  value  c  and  list  item  x):
                                add  f[x]  c
                              over  list:
                                  v
                              with  starting  value:
                                x);accumulate  (with  value  c  and  list  item  x):
                                        add  g[x]  c
                                      over  list:
                                          v
                                      with  starting  value:
                                        y)]))
12.  x  :  R
13.  y  :  R
14.  z  :  R
15.  z  =  add[x;y]
\mvdash{}  (((f  u)  add  (g  u))  add  (x  add  y))  =  (((f  u)  add  x)  add  ((g  u)  add  y))


By

---

Latex:
(D  7
  THEN  Unfold  `assoc`  7
  THEN  (RWO  "7"  0  THEN  Auto  THEN  EqCD  THEN  Auto)
  THEN  RWO  "7<"  0
  THEN  Auto
  THEN  EqCD
  THEN  Auto)

---

Home Index