---

Step * of Lemma bag-mapfilter-fast-map

∀[bs:bag(Top)]. ∀[P,f,g:Top].  (bag-mapfilter-fast(f;P;bag-map(g;bs)) ~ bag-mapfilter-fast(f o g;P o g;bs))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``bag-mapfilter-fast bag-accum bag-map`` 0
   THEN (RWO "list_accum-map" 0 THENA Auto)
   THEN RepUR ``compose so_apply`` 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[bs:bag(Top)].  \mforall{}[P,f,g:Top].
    (bag-mapfilter-fast(f;P;bag-map(g;bs))  \msim{}  bag-mapfilter-fast(f  o  g;P  o  g;bs))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``bag-mapfilter-fast  bag-accum  bag-map``  0
  THEN  (RWO  "list\_accum-map"  0  THENA  Auto)
  THEN  RepUR  ``compose  so\_apply``  0
  THEN  Auto)

---

Home Index