---

Step * 1 1 of Lemma mapfilter-subbag

.....equality..... 
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)
⊢ (λx.((P x) ∨b((¬b(P x)) ∧b (Q x)))) = Q ∈ (T ─→ 𝔹)
BY
{ (Ext THEN Reduce 0 THEN Auto THEN AutoBoolCase ⌈P x⌉⋅) }

---

Latex:

---

Latex:
.....equality..... 
1.  T  :  Type@i'
2.  U  :  Type@i'
3.  f  :  T  {}\mrightarrow{}  U@i
4.  P  :  T  {}\mrightarrow{}  \mBbbB{}@i
5.  Q  :  T  {}\mrightarrow{}  \mBbbB{}@i
6.  L  :  T  List@i
7.  \mforall{}t:T.  ((\muparrow{}(P  t))  {}\mRightarrow{}  (\muparrow{}(Q  t)))@i
8.  (mapfilter(f;P;L)  @  mapfilter(f;\mlambda{}x.((\mneg{}\msubb{}(P  x))  \mwedge{}\msubb{}  (Q  x));L))
=  (mapfilter(f;\mlambda{}x.((P  x)  \mvee{}\msubb{}((\mneg{}\msubb{}(P  x))  \mwedge{}\msubb{}  (Q  x)));L)
    @  mapfilter(f;\mlambda{}x.((P  x)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(P  x))  \mwedge{}\msubb{}  (Q  x));L))
\mvdash{}  (\mlambda{}x.((P  x)  \mvee{}\msubb{}((\mneg{}\msubb{}(P  x))  \mwedge{}\msubb{}  (Q  x))))  =  Q


By

---

Latex:
(Ext  THEN  Reduce  0  THEN  Auto  THEN  AutoBoolCase  \mkleeneopen{}P  x\mkleeneclose{}\mcdot{})

---

Home Index