---

Step * 1 of Lemma bag-count-combine


1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq : EqDecider(T2)
5. z : T2
6. L : T1 List
⊢ (#z in ⋃x∈L.f[x]) = bag-sum(L;x.(#z in f[x])) ∈ ℕ
BY
{ (RepUR ``bag-combine bag-union bag-sum bag-map`` 0
   THEN MoveToConcl (-1)
   THEN InductionOnLast
   THEN (RWW "list_accum_append map_append_sq concat_append" 0 THENA Auto)
   THEN Reduce 0
   THEN RWW "concat-single bag-count-append" 0
   THEN Auto)⋅ }

1
1. T1 : Type
2. T2 : Type
3. f : T1 ⟶ bag(T2)
4. eq : EqDecider(T2)
5. z : T2
6. L : T1 List
7. ¬↑null(L)
8. ||L|| ≥ 1 
9. (#z in concat(map(λx.f[x];firstn(||L|| - 1;L))))
= accumulate (with value s and list item x):
   (#z in f[x]) + s
  over list:
    firstn(||L|| - 1;L)
  with starting value:
   0)
∈ ℕ
⊢ (#z in concat(map(λx.f[x];firstn(||L|| - 1;L))) @ f[last(L)])
= ((#z in f[last(L)])
  + accumulate (with value s and list item x):
     (#z in f[x]) + s
    over list:
      firstn(||L|| - 1;L)
    with starting value:
     0))
∈ ℕ

---

Latex:

---

Latex:

1.  T1  :  Type
2.  T2  :  Type
3.  f  :  T1  {}\mrightarrow{}  bag(T2)
4.  eq  :  EqDecider(T2)
5.  z  :  T2
6.  L  :  T1  List
\mvdash{}  (\#z  in  \mcup{}x\mmember{}L.f[x])  =  bag-sum(L;x.(\#z  in  f[x]))


By

---

Latex:
(RepUR  ``bag-combine  bag-union  bag-sum  bag-map``  0
  THEN  MoveToConcl  (-1)
  THEN  InductionOnLast
  THEN  (RWW  "list\_accum\_append  map\_append\_sq  concat\_append"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RWW  "concat-single  bag-count-append"  0
  THEN  Auto)\mcdot{}

---

Home Index