---

Step * of Lemma bag-mapfilter-fast-eq

∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B].
  (bag-mapfilter-fast(f;P;bs) = bag-mapfilter(f;P;bs) ∈ bag(B))
BY
{ (Auto
   THEN RepUR ``bag-mapfilter`` 0
   THEN (InstLemma `bag-map-as-accum` [⌜{x:A| ↑P[x]} ⌝;⌜B⌝;⌜f⌝;⌜[x∈bs|P x]⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (InstLemma `bag-filter-as-accum` [⌜A⌝;⌜P⌝;⌜bs⌝]⋅ THENA Auto)
   THEN (RWO "-1" 0
         THENA (Auto
                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)
         )
   THEN RepeatFor 2 (Thin (-1))) }

1
1. A : Type
2. B : Type
3. bs : bag(A)
4. P : A ⟶ 𝔹
5. f : {x:A| ↑P[x]}  ⟶ B
⊢ bag-mapfilter-fast(f;P;bs) = bag-accum(b,x.f[x].b;{};bag-accum(b,x.if P[x] then x.b else b fi ;{};bs)) ∈ bag(B)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[bs:bag(A)].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:A|  \muparrow{}P[x]\}    {}\mrightarrow{}  B].
    (bag-mapfilter-fast(f;P;bs)  =  bag-mapfilter(f;P;bs))


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-mapfilter``  0
  THEN  (InstLemma  `bag-map-as-accum`  [\mkleeneopen{}\{x:A|  \muparrow{}P[x]\}  \mkleeneclose{};\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}[x\mmember{}bs|P  x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (InstLemma  `bag-filter-as-accum`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0
              THENA  (Auto
                            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)
              )
  THEN  RepeatFor  2  (Thin  (-1)))

---

Home Index