---

Step * of Lemma bag-mapfilter-fast_wf

∀[A,B:Type]. ∀[bs:bag(A)]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑P[x]}  ⟶ B].  (bag-mapfilter-fast(f;P;bs) ∈ bag(B))
BY
{ (ProveWfLemma
   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:
\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)  \mmember{}  bag(B))


By

---

Latex:
(ProveWfLemma
  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