---

Step * 1 1 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
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)
∈ ℕ
10. b : bag(T1)
11. firstn(||L|| - 1;L) = b ∈ bag(T1)
12. c : bag(T2)
13. f[last(L)] = c ∈ bag(T2)
14. d : bag(T2)
15. bag-union(bag-map(λx.f[x];b)) = d ∈ bag(T2)
⊢ (#z in d + c) = ((#z in c) + (#z in d)) ∈ ℕ
BY
{ (All Thin THEN EqTypeCD THEN Auto')⋅ }

---

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
7.  \mneg{}\muparrow{}null(L)
8.  ||L||  \mgeq{}  1 
9.  (\#z  in  concat(map(\mlambda{}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)
10.  b  :  bag(T1)
11.  firstn(||L||  -  1;L)  =  b
12.  c  :  bag(T2)
13.  f[last(L)]  =  c
14.  d  :  bag(T2)
15.  bag-union(bag-map(\mlambda{}x.f[x];b))  =  d
\mvdash{}  (\#z  in  d  +  c)  =  ((\#z  in  c)  +  (\#z  in  d))


By

---

Latex:
(All  Thin  THEN  EqTypeCD  THEN  Auto')\mcdot{}

---

Home Index