---

Step * of Lemma mapfilter-bor

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

---

Latex:

---

Latex:
\mforall{}T,U:Type.  \mforall{}f:T  {}\mrightarrow{}  U.  \mforall{}P,Q:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.
    sub-bag(U;mapfilter(f;\mlambda{}x.(P[x]  \mvee{}\msubb{}Q[x]);L);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.(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{}Q\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index