---

Step * 1 of Lemma bag-map-as-accum


1. A : Type
2. B : Type
3. f : A ⟶ B
4. u : A
5. v : A List
6. ({u} + v) = (v + {u}) ∈ bag(A)
⊢ ({f u} + bag-accum(b,x.f[x].b;{};v)) = bag-accum(b,x.{f[x]} + b;bag-accum(b,x.{f[x]} + b;{};v);{u}) ∈ bag(B)
BY
{ ((RWO "bag-accum-single" 0 THENA Auto)
   THEN RepUR ``so_apply`` 0
   THEN (MemCD THEN Auto)
   THEN RWO "cons-bag-as-append" 0
   THEN Auto
   THEN (RWO "bag-append-assoc<" 0 THENA Auto)
   THEN (MemCD THEN Auto)
   THEN BLemma `bag-append-comm`
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "bag-accum-single"  0  THENA  Auto)
  THEN  RepUR  ``so\_apply``  0
  THEN  (MemCD  THEN  Auto)
  THEN  RWO  "cons-bag-as-append"  0
  THEN  Auto
  THEN  (RWO  "bag-append-assoc<"  0  THENA  Auto)
  THEN  (MemCD  THEN  Auto)
  THEN  BLemma  `bag-append-comm`
  THEN  Auto)

---

Home Index