---

Step * 1 of Lemma bag-summation-linear


1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. mul : R ⟶ R ⟶ R
5. zero : R
6. f : T ⟶ R
7. g : T ⟶ R
8. minus : R ⟶ R
9. IsGroup(R;add;zero;minus)
10. Comm(R;add)
11. BiLinear(R;add;mul)
12. a : R
13. L : T List
⊢ Σ(x∈L). a mul (f[x] add g[x]) = (a mul (Σ(x∈L). f[x] add Σ(x∈L). g[x])) ∈ R
BY
{ (RepUR ``bag-summation bag-accum`` 0
   THEN Assert ⌜∀x,y,z:R.
                  ((z = mul[a;add[x;y]] ∈ R)
                  ⇒ (accumulate (with value c and list item x):
                       add mul[a;add[f[x];g[x]]] c
                      over list:
                        L
                      with starting value:
                       z)
                     = mul[a;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))⌝⋅
   ) }

1
.....assertion..... 
1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. mul : R ⟶ R ⟶ R
5. zero : R
6. f : T ⟶ R
7. g : T ⟶ R
8. minus : R ⟶ R
9. IsGroup(R;add;zero;minus)
10. Comm(R;add)
11. BiLinear(R;add;mul)
12. a : R
13. L : T List
⊢ ∀x,y,z:R.
    ((z = mul[a;add[x;y]] ∈ R)
    ⇒ (accumulate (with value c and list item x):
         add mul[a;add[f[x];g[x]]] c
        over list:
          L
        with starting value:
         z)
       = mul[a;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))

2
1. T : Type
2. R : Type
3. add : R ⟶ R ⟶ R
4. mul : R ⟶ R ⟶ R
5. zero : R
6. f : T ⟶ R
7. g : T ⟶ R
8. minus : R ⟶ R
9. IsGroup(R;add;zero;minus)
10. Comm(R;add)
11. BiLinear(R;add;mul)
12. a : R
13. L : T List
14. ∀x,y,z:R.
      ((z = mul[a;add[x;y]] ∈ R)
      ⇒ (accumulate (with value c and list item x):
           add mul[a;add[f[x];g[x]]] c
          over list:
            L
          with starting value:
           z)
         = mul[a;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))
⊢ accumulate (with value c and list item x):
   add (a mul (f[x] add g[x])) c
  over list:
    L
  with starting value:
   zero)
= (a 
   mul 
   (accumulate (with value c and list item x):
     add f[x] c
    over list:
      L
    with starting value:
     zero) 
    add 
    accumulate (with value c and list item x):
     add g[x] c
    over list:
      L
    with starting value:
     zero)))
∈ R

---

Latex:

---

Latex:

1.  T  :  Type
2.  R  :  Type
3.  add  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
4.  mul  :  R  {}\mrightarrow{}  R  {}\mrightarrow{}  R
5.  zero  :  R
6.  f  :  T  {}\mrightarrow{}  R
7.  g  :  T  {}\mrightarrow{}  R
8.  minus  :  R  {}\mrightarrow{}  R
9.  IsGroup(R;add;zero;minus)
10.  Comm(R;add)
11.  BiLinear(R;add;mul)
12.  a  :  R
13.  L  :  T  List
\mvdash{}  \mSigma{}(x\mmember{}L).  a  mul  (f[x]  add  g[x])  =  (a  mul  (\mSigma{}(x\mmember{}L).  f[x]  add  \mSigma{}(x\mmember{}L).  g[x]))


By

---

Latex:
(RepUR  ``bag-summation  bag-accum``  0
  THEN  Assert  \mkleeneopen{}\mforall{}x,y,z:R.
                                ((z  =  mul[a;add[x;y]])
                                {}\mRightarrow{}  (accumulate  (with  value  c  and  list  item  x):
                                          add  mul[a;add[f[x];g[x]]]  c
                                        over  list:
                                            L
                                        with  starting  value:
                                          z)
                                      =  mul[a;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)]]))\mkleeneclose{}\mcdot{}
  )

---

Home Index