---

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


1. L : ℤ List
⊢ reduce(λx,y. (x * y);1;L) = accumulate (with value c and list item x): x * cover list:  Lwith starting value: 1) ∈ ℤ
BY
{ xxxAssert ⌜∀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))
               ∈ ℤ)⌝⋅xxx }

1
.....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))
    ∈ ℤ)

2
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) ∈ ℤ

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
\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:
xxxAssert  \mkleeneopen{}\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)))\mkleeneclose{}\mcdot{}xxx

---

Home Index