---

Step * 1 2 of Lemma mul-list-bag-product


1. L : ℤ List
2. ∀x:ℤ
     (accumulate (with value c and list item p):
       p * c
      over list:
        L
      with starting value:
       x)
     = (x * reduce(λx,y. (x * y);1;L))
     ∈ ℤ)
⊢ reduce(λx,y. (x * y);1;L) = accumulate (with value c and list item x): x * cover list:  Lwith starting value: 1) ∈ ℤ
BY
{ xxx(RWO "-1" 0 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  \mforall{}x:\mBbbZ{}
          (accumulate  (with  value  c  and  list  item  p):
              p  *  c
            over  list:
                L
            with  starting  value:
              x)
          =  (x  *  reduce(\mlambda{}x,y.  (x  *  y);1;L)))
\mvdash{}  reduce(\mlambda{}x,y.  (x  *  y);1;L)
=  accumulate  (with  value  c  and  list  item  x):
      x  *  c
    over  list:
        L
    with  starting  value:
      1)


By

---

Latex:
xxx(RWO  "-1"  0  THEN  Auto)xxx

---

Home Index