---

Step * 1 2 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;Q;L) @ mapfilter(f;λx.ff;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 ⌈mapfilter(f;λx.ff;L) ~ []⌉ (-1)⋅ }

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;Q;L) @ mapfilter(f;λx.ff;L)) ∈ bag(U)
⊢ mapfilter(f;λx.ff;L) ~ []

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) @ []) ∈ 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;Q;L)  @  mapfilter(f;\mlambda{}x.ff;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{}mapfilter(f;\mlambda{}x.ff;L)  \msim{}  []\mkleeneclose{}  (-1)\mcdot{}

---

Home Index