---

Step * of Lemma sub-bag-mapfilter-implies

∀[A,B:Type].
  ∀as:bag(A). ∀bs:bag(B). ∀f:A ⟶ B. ∀P:A ⟶ 𝔹.  (sub-bag(B;bag-map(f;as);bs) ⇒ sub-bag(B;bag-mapfilter(f;P;as);bs))
BY
{ (Auto
   THEN All(RepUR ``sub-bag bag-mapfilter``)
   THEN ExRepD
   THEN (InstLemma `bag-filter-split` [⌜A⌝;⌜P⌝;⌜as⌝]⋅ THENA Auto)
   THEN (RevHypSubst (-1) (-2) THENA Auto)
   THEN (RWO "bag-map-append" (-2) THENA Auto)
   THEN InstConcl [⌜bag-map(f;[x∈as|¬bP[x]]) + cs⌝]⋅
   THEN Auto
   THEN RWO "bag-append-assoc<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}as:bag(A).  \mforall{}bs:bag(B).  \mforall{}f:A  {}\mrightarrow{}  B.  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.
        (sub-bag(B;bag-map(f;as);bs)  {}\mRightarrow{}  sub-bag(B;bag-mapfilter(f;P;as);bs))


By

---

Latex:
(Auto
  THEN  All(RepUR  ``sub-bag  bag-mapfilter``)
  THEN  ExRepD
  THEN  (InstLemma  `bag-filter-split`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RevHypSubst  (-1)  (-2)  THENA  Auto)
  THEN  (RWO  "bag-map-append"  (-2)  THENA  Auto)
  THEN  InstConcl  [\mkleeneopen{}bag-map(f;[x\mmember{}as|\mneg{}\msubb{}P[x]])  +  cs\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  RWO  "bag-append-assoc<"  0
  THEN  Auto)

---

Home Index