---

Step * 2 1 1 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)
7. ({u} + v) = (v + {u}) ∈ bag(A)
⊢ (f[u] + bag-accum(c,b.f[b] + c;{};v)) = bag-accum(c,b.f[b] + c;{};v + {u}) ∈ bag(B)
BY
{ (RepUR ``bag-accum bag-append`` 0
   THEN (RWO "list_accum_append" 0 THENA (Auto THEN Unfold `single-bag` 0 THEN Auto))
   THEN Try (Folds ``bag-accum bag-append`` 0)
   THEN RWO "bag-accum-single" 0
   THEN Auto) }

---

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)
7.  (\{u\}  +  v)  =  (v  +  \{u\})
\mvdash{}  (f[u]  +  bag-accum(c,b.f[b]  +  c;\{\};v))  =  bag-accum(c,b.f[b]  +  c;\{\};v  +  \{u\})


By

---

Latex:
(RepUR  ``bag-accum  bag-append``  0
  THEN  (RWO  "list\_accum\_append"  0  THENA  (Auto  THEN  Unfold  `single-bag`  0  THEN  Auto))
  THEN  Try  (Folds  ``bag-accum  bag-append``  0)
  THEN  RWO  "bag-accum-single"  0
  THEN  Auto)

---

Home Index