---

Step * of Lemma bag-mapfilter-map

∀[A,B,C:Type]. ∀[b:bag(A)]. ∀[P:B ⟶ 𝔹]. ∀[f:{x:B| ↑P[x]}  ⟶ C]. ∀[g:A ⟶ B].
  (bag-mapfilter(f;P;bag-map(g;b)) = bag-mapfilter(f o g;P o g;b) ∈ bag(C))
BY
{ (Auto
   THEN RepUR ``bag-mapfilter`` 0
   THEN (RWO "bag-filter-map2" 0
         THENA (Try (Complete (Auto))
                THEN Try (Fold `member` 0)
                THEN Using [`A',⌜{x:A| ↑(P (g x))} ⌝;`B',⌜C⌝] (BLemma `bag-map_wf`)⋅
                THEN Try (Complete (Auto))
                THEN Unfold `compose` 0
                THEN (MemCD THENA Auto)
                THEN D (-1)
                THEN Auto)
         )
   THEN (RWO "bag-map-map" 0 THENA (Auto THEN DoSubsume THEN Auto))
   THEN Try (Fold `member` 0)
   THEN Using [`A',⌜{x:A| ↑(P (g x))} ⌝;`B',⌜C⌝] (BLemma `bag-map_wf`)⋅
   THEN Try (Complete (Auto))
   THEN Unfold `compose` 0
   THEN (MemCD THENA Auto)
   THEN D (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].  \mforall{}[b:bag(A)].  \mforall{}[P:B  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:\{x:B|  \muparrow{}P[x]\}    {}\mrightarrow{}  C].  \mforall{}[g:A  {}\mrightarrow{}  B].
    (bag-mapfilter(f;P;bag-map(g;b))  =  bag-mapfilter(f  o  g;P  o  g;b))


By

---

Latex:
(Auto
  THEN  RepUR  ``bag-mapfilter``  0
  THEN  (RWO  "bag-filter-map2"  0
              THENA  (Try  (Complete  (Auto))
                            THEN  Try  (Fold  `member`  0)
                            THEN  Using  [`A',\mkleeneopen{}\{x:A|  \muparrow{}(P  (g  x))\}  \mkleeneclose{};`B',\mkleeneopen{}C\mkleeneclose{}]  (BLemma  `bag-map\_wf`)\mcdot{}
                            THEN  Try  (Complete  (Auto))
                            THEN  Unfold  `compose`  0
                            THEN  (MemCD  THENA  Auto)
                            THEN  D  (-1)
                            THEN  Auto)
              )
  THEN  (RWO  "bag-map-map"  0  THENA  (Auto  THEN  DoSubsume  THEN  Auto))
  THEN  Try  (Fold  `member`  0)
  THEN  Using  [`A',\mkleeneopen{}\{x:A|  \muparrow{}(P  (g  x))\}  \mkleeneclose{};`B',\mkleeneopen{}C\mkleeneclose{}]  (BLemma  `bag-map\_wf`)\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  Unfold  `compose`  0
  THEN  (MemCD  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto)

---

Home Index