---

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


1. A : Type
2. B : Type
3. P : A ⟶ 𝔹
4. f : {x:A| ↑P[x]}  ⟶ B
⊢ bag-accum(b,x.if P[x] then f[x].b else b fi ;{};[])
= bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};[]))
∈ bag(B)
BY
{ (RepUR ``bag-accum empty-bag`` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  P  :  A  {}\mrightarrow{}  \mBbbB{}
4.  f  :  \{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B
\mvdash{}  bag-accum(b,x.if  P[x]  then  f[x].b  else  b  fi  ;\{\};[])
=  bag-accum(b,x.f[x].b;\{\};bag-accum(b,x.if  P[x]  then  x.b  else  b  fi  ;\{\};[]))


By

---

Latex:
(RepUR  ``bag-accum  empty-bag``  0  THEN  Auto)

---

Home Index