---

Step * 1 of Lemma bag-sum-count


1. A : Type
2. B : Type
3. f : B ⟶ bag(A)
4. eq : EqDecider(A)
5. z : A
6. as : B List
7. bs : B List
8. permutation(B;as;bs)
⊢ bag-sum(bs;b.(#z in f[b])) = bag-sum([b∈bs|1 ≤z (#z in f[b])];b.(#z in f[b])) ∈ ℤ
BY
{ xxx((ThinVar `as' THEN RepUR ``bag-sum bag-filter`` 0)
      THEN MoveToConcl (-1)
      THEN InductionOnLast
      THEN Reduce 0
      THEN Auto
      THEN (RWW "filter_append list_accum_append" 0 THENA Auto)
      THEN Reduce 0
      THEN RevHypSubst' (-1) 0
      THEN GenConclAtAddr [2;2]
      THEN AutoSplit
      THEN RepUR ``eqof`` -1)xxx }

1
1. A : Type
2. B : Type
3. f : B ⟶ bag(A)
4. eq : EqDecider(A)
5. z : A
6. bs : B List
7. ¬(1 ≤ (#z in f[last(bs)]))
8. ¬↑null(bs)
9. ||bs|| ≥ 1 
10. accumulate (with value s and list item b):
     (#z in f[b]) + s
    over list:
      firstn(||bs|| - 1;bs)
    with starting value:
     0)
= accumulate (with value s and list item b):
   (#z in f[b]) + s
  over list:
    filter(λb.1 ≤z (#z in f[b]);firstn(||bs|| - 1;bs))
  with starting value:
   0)
∈ ℤ
11. v : ℤ
12. accumulate (with value s and list item b):
     (#z in f[b]) + s
    over list:
      firstn(||bs|| - 1;bs)
    with starting value:
     0)
= v
∈ ℤ
⊢ ((#z in f[last(bs)]) + v) = v ∈ ℤ

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  B  {}\mrightarrow{}  bag(A)
4.  eq  :  EqDecider(A)
5.  z  :  A
6.  as  :  B  List
7.  bs  :  B  List
8.  permutation(B;as;bs)
\mvdash{}  bag-sum(bs;b.(\#z  in  f[b]))  =  bag-sum([b\mmember{}bs|1  \mleq{}z  (\#z  in  f[b])];b.(\#z  in  f[b]))


By

---

Latex:
xxx((ThinVar  `as'  THEN  RepUR  ``bag-sum  bag-filter``  0)
        THEN  MoveToConcl  (-1)
        THEN  InductionOnLast
        THEN  Reduce  0
        THEN  Auto
        THEN  (RWW  "filter\_append  list\_accum\_append"  0  THENA  Auto)
        THEN  Reduce  0
        THEN  RevHypSubst'  (-1)  0
        THEN  GenConclAtAddr  [2;2]
        THEN  AutoSplit
        THEN  RepUR  ``eqof``  -1)xxx

---

Home Index