---

Step * 1 4 of Lemma bag-mapfilter-fast-eq


1. A : Type
2. B : Type
3. L : A List
4. bs : bag(A)
5. P : A ⟶ 𝔹
6. f : {x:A| ↑P[x]}  ⟶ B
7. bs = L ∈ bag(A)
8. z : bag(A)
⊢ bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};z)) ∈ bag(B)
BY
{ (Using [`T',⌜{x:A| ↑P[x]} ⌝] (BLemma `bag-accum_wf`)⋅
   THEN Auto
   THEN Repeat (AutoSplit)
   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.  B  :  Type
3.  L  :  A  List
4.  bs  :  bag(A)
5.  P  :  A  {}\mrightarrow{}  \mBbbB{}
6.  f  :  \{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B
7.  bs  =  L
8.  z  :  bag(A)
\mvdash{}  bag-accum(b,x.f[x].b;\{\};bag-accum(b,x.if  P[x]  then  x.b  else  b  fi  ;\{\};z))  \mmember{}  bag(B)


By

---

Latex:
(Using  [`T',\mkleeneopen{}\{x:A|  \muparrow{}P[x]\}  \mkleeneclose{}]  (BLemma  `bag-accum\_wf`)\mcdot{}
  THEN  Auto
  THEN  Repeat  (AutoSplit)
  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