---

Step * of Lemma mapfilter-subbag

∀T,U:Type. ∀f:T ⟶ U. ∀P,Q:T ⟶ 𝔹. ∀L:T List.
  ((∀t:T. ((↑(P t)) ⇒ (↑(Q t)))) ⇒ sub-bag(U;mapfilter(f;P;L);mapfilter(f;Q;L)))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `sub-bag` 0
   THEN (InstConcl [⌜mapfilter(f;λx.((¬bP[x]) ∧b Q[x]);L)⌝]⋅ THENA Auto)
   THEN Unfold `bag-append` 0
   THEN InstLemma `mapfilter-bor-eq` [⌜T⌝;⌜U⌝;⌜f⌝;⌜P⌝;⌜λx.((¬bP[x]) ∧b Q[x])⌝;⌜L⌝]⋅
   THEN Auto
   THEN All (RepUR ``so_apply``)) }

1
1. T : Type@i'
2. U : Type@i'
3. f : T ⟶ U@i
4. P : T ⟶ 𝔹@i
5. Q : T ⟶ 𝔹@i
6. L : T List@i
7. ∀t:T. ((↑(P t)) ⇒ (↑(Q t)))@i
8. (mapfilter(f;P;L) @ mapfilter(f;λx.((¬b(P x)) ∧b (Q x));L))
= (mapfilter(f;λx.((P x) ∨b((¬b(P x)) ∧b (Q x)));L) @ mapfilter(f;λx.((P x) ∧b (¬b(P x)) ∧b (Q x));L))
∈ bag(U)
⊢ mapfilter(f;Q;L) = (mapfilter(f;P;L) @ mapfilter(f;λx.((¬b(P x)) ∧b (Q x));L)) ∈ bag(U)

---

Latex:

---

Latex:
\mforall{}T,U:Type.  \mforall{}f:T  {}\mrightarrow{}  U.  \mforall{}P,Q:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.
    ((\mforall{}t:T.  ((\muparrow{}(P  t))  {}\mRightarrow{}  (\muparrow{}(Q  t))))  {}\mRightarrow{}  sub-bag(U;mapfilter(f;P;L);mapfilter(f;Q;L)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `sub-bag`  0
  THEN  (InstConcl  [\mkleeneopen{}mapfilter(f;\mlambda{}x.((\mneg{}\msubb{}P[x])  \mwedge{}\msubb{}  Q[x]);L)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Unfold  `bag-append`  0
  THEN  InstLemma  `mapfilter-bor-eq`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}U\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}\mlambda{}x.((\mneg{}\msubb{}P[x])  \mwedge{}\msubb{}  Q[x])\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  All  (RepUR  ``so\_apply``))

---

Home Index