---

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


1. A : Type
2. p : A ⟶ 𝔹
3. u : A
4. v : A List
5. ↑p[u]
6. ↑p[u]
⊢ ({u} + bag-accum(b,x.if p[x] then x.b else b fi ;{};v))
= ({u} + bag-accum(b,x.if p[x] then {x} + b else b fi ;{};v))
∈ bag({x:A| ↑p[x]} )
BY
{ (RWO "cons-bag-as-append" 0
   THEN Auto
   THEN Repeat OldAutoSplit
   THEN Repeat ((RWO "cons-bag-as-append" 0 THENA 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.  p  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  \muparrow{}p[u]
6.  \muparrow{}p[u]
\mvdash{}  (\{u\}  +  bag-accum(b,x.if  p[x]  then  x.b  else  b  fi  ;\{\};v))
=  (\{u\}  +  bag-accum(b,x.if  p[x]  then  \{x\}  +  b  else  b  fi  ;\{\};v))


By

---

Latex:
(RWO  "cons-bag-as-append"  0
  THEN  Auto
  THEN  Repeat  OldAutoSplit
  THEN  Repeat  ((RWO  "cons-bag-as-append"  0  THENA  Auto))
  THEN  (RWO  "bag-append-assoc<"  0  THENA  Auto)
  THEN  (MemCD  THEN  Auto)
  THEN  BLemma  `bag-append-comm`
  THEN  Auto)

---

Home Index