---

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

.....assertion..... 
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. L : T List
⊢ ∀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:
          L
        with starting value:
         z)
       = add[accumulate (with value c and list item x):
              add f[x] c
             over list:
               L
             with starting value:
              x);accumulate (with value c and list item x):
                  add g[x] c
                 over list:
                   L
                 with starting value:
                  y)]
       ∈ R))
BY
{ (ListInd (-1) THEN Reduce 0) }

1
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)
⊢ ∀x,y,z:R.  ((z = add[x;y] ∈ R) ⇒ (z = add[x;y] ∈ R))

2
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))
⊢ ∀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:
         add add[f[u];g[u]] z)
       = add[accumulate (with value c and list item x):
              add f[x] c
             over list:
               v
             with starting value:
              add f[u] x);accumulate (with value c and list item x):
                           add g[x] c
                          over list:
                            v
                          with starting value:
                           add g[u] y)]
       ∈ R))

---

Latex:

---

Latex:
.....assertion..... 
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.  L  :  T  List
\mvdash{}  \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:
                    L
                with  starting  value:
                  z)
              =  add[accumulate  (with  value  c  and  list  item  x):
                            add  f[x]  c
                          over  list:
                              L
                          with  starting  value:
                            x);accumulate  (with  value  c  and  list  item  x):
                                    add  g[x]  c
                                  over  list:
                                      L
                                  with  starting  value:
                                    y)]))


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0)

---

Home Index