---

Step * of Lemma filter-filter2

∀[P1,P2,L:Top].  (filter(P2;filter(P1;L)) ~ filter(λt.((P1 t) ∧b (P2 t));L))
BY
{ (RWO "filter-filter" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[P1,P2,L:Top].    (filter(P2;filter(P1;L))  \msim{}  filter(\mlambda{}t.((P1  t)  \mwedge{}\msubb{}  (P2  t));L))


By

---

Latex:
(RWO  "filter-filter"  0  THEN  Auto)

---

Home Index