---

Step * 1 of Lemma mapfilter-subbag


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)
BY
{ (Subst ⌈(λx.((P x) ∨b((¬b(P x)) ∧b (Q x)))) = Q ∈ (T ─→ 𝔹)⌉ (-1)⋅ THENA Auto) }

1
.....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 ─→ 𝔹)

2
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;Q;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:

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{}  mapfilter(f;Q;L)  =  (mapfilter(f;P;L)  @  mapfilter(f;\mlambda{}x.((\mneg{}\msubb{}(P  x))  \mwedge{}\msubb{}  (Q  x));L))


By

---

Latex:
(Subst  \mkleeneopen{}(\mlambda{}x.((P  x)  \mvee{}\msubb{}((\mneg{}\msubb{}(P  x))  \mwedge{}\msubb{}  (Q  x))))  =  Q\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)

---

Home Index