---

Step * of Lemma mapfilter-mapfilter

∀[f1,as,P2,f2,P1:Top].  (mapfilter(f1;P1;mapfilter(f2;P2;as)) ~ mapfilter(f1 o f2;λa.((P2 a) ∧b (P1 (f2 a)));as))
BY
{ ((UnivCD⋅ THENA Auto)
   THEN Unfold `mapfilter` 0
   THEN (RWW "filter-map map-map filter-filter" 0 THENA Auto)
   THEN RepUR ``compose`` 0
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[f1,as,P2,f2,P1:Top].
    (mapfilter(f1;P1;mapfilter(f2;P2;as))  \msim{}  mapfilter(f1  o  f2;\mlambda{}a.((P2  a)  \mwedge{}\msubb{}  (P1  (f2  a)));as))


By

---

Latex:
((UnivCD\mcdot{}  THENA  Auto)
  THEN  Unfold  `mapfilter`  0
  THEN  (RWW  "filter-map  map-map  filter-filter"  0  THENA  Auto)
  THEN  RepUR  ``compose``  0
  THEN  Trivial)

---

Home Index