---

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

.....assertion..... 
1. L : ℤ List
⊢ ∀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))
    ∈ ℤ)
BY
{ xxx(ListInd 1 THEN Reduce 0 THEN Auto THEN RWO "-2" 0 THEN Auto)xxx }

---

Latex:

---

Latex:
.....assertion..... 
1.  L  :  \mBbbZ{}  List
\mvdash{}  \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)))


By

---

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

---

Home Index