---

Step * 2 of Lemma bag-combine-as-accum


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. u : A
5. v : A List
6. ⋃b∈v.f[b] = bag-accum(c,b.f[b] + c;{};v) ∈ bag(B)
⊢ ⋃b∈[u / v].f[b] = bag-accum(c,b.f[b] + c;{};[u / v]) ∈ bag(B)
BY
{ (Fold `cons-bag` 0 THEN (RWO "bag-combine-cons-left" 0 THENA Auto) THEN (RWO  "-1" 0 THENA Auto)) }

1
1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. u : A
5. v : A List
6. ⋃b∈v.f[b] = bag-accum(c,b.f[b] + c;{};v) ∈ bag(B)
⊢ (f[u] + bag-accum(c,b.f[b] + c;{};v)) = bag-accum(c,b.f[b] + c;{};u.v) ∈ bag(B)

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  u  :  A
5.  v  :  A  List
6.  \mcup{}b\mmember{}v.f[b]  =  bag-accum(c,b.f[b]  +  c;\{\};v)
\mvdash{}  \mcup{}b\mmember{}[u  /  v].f[b]  =  bag-accum(c,b.f[b]  +  c;\{\};[u  /  v])


By

---

Latex:
(Fold  `cons-bag`  0  THEN  (RWO  "bag-combine-cons-left"  0  THENA  Auto)  THEN  (RWO    "-1"  0  THENA  Auto))

---

Home Index