---

Step * of Lemma bag-summation-constant

∀[T:Type]. ∀[r:Rng]. ∀[b:bag(T)].  ∀a:|r|. (Σ(x∈b). a = (#(b) ⋅r a) ∈ |r|)
BY
{ (Auto
   THEN (BagToList (-2) THENA Auto)
   THEN RepUR ``bag-size bag-summation bag-accum rng_nat_op mon_nat_op nat_op`` 0
   THEN (Assert ⌜∀x:|r|
                   (accumulate (with value c and list item x):
                     +r a c
                    over list:
                      b
                    with starting value:
                     x)
                   = (+r x Π(+r,0) 0 ≤ i < ||b||. a)
                   ∈ |r|)⌝⋅
   THENM (RWO "-1" 0 THEN Auto THEN RW RngNormC 0 THEN Auto)
   )) }

1
.....assertion..... 
1. T : Type
2. r : Rng
3. b : T List
4. a : |r|
⊢ ∀x:|r|
    (accumulate (with value c and list item x):
      +r a c
     over list:
       b
     with starting value:
      x)
    = (+r x Π(+r,0) 0 ≤ i < ||b||. a)
    ∈ |r|)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[r:Rng].  \mforall{}[b:bag(T)].    \mforall{}a:|r|.  (\mSigma{}(x\mmember{}b).  a  =  (\#(b)  \mcdot{}r  a))


By

---

Latex:
(Auto
  THEN  (BagToList  (-2)  THENA  Auto)
  THEN  RepUR  ``bag-size  bag-summation  bag-accum  rng\_nat\_op  mon\_nat\_op  nat\_op``  0
  THEN  (Assert  \mkleeneopen{}\mforall{}x:|r|
                                  (accumulate  (with  value  c  and  list  item  x):
                                      +r  a  c
                                    over  list:
                                        b
                                    with  starting  value:
                                      x)
                                  =  (+r  x  \mPi{}(+r,0)  0  \mleq{}  i  <  ||b||.  a))\mkleeneclose{}\mcdot{}
  THENM  (RWO  "-1"  0  THEN  Auto  THEN  RW  RngNormC  0  THEN  Auto)
  ))

---

Home Index