---

Step * of Lemma reduce-mapfilter

∀[f1,x:Top]. ∀[T,A:Type]. ∀[as:T List]. ∀[P:{a:T| (a ∈ as)}  ⟶ 𝔹]. ∀[f2:{a:T| (a ∈ as) ∧ (↑(P a))}  ⟶ A].
  (reduce(f1;x;mapfilter(f2;P;as)) ~ reduce(λu,z. if P u then f1 (f2 u) z else z fi ;x;as))
BY
{ ((UnivCD THENA Auto)
   THEN ListInd (-3)
   THEN RepUR ``mapfilter`` 0
   THEN (RepeatFor 2 ((D 0 THENA Auto))
         THEN Try (Trivial)
         THEN (InstHyp [⌜P⌝;⌜f2⌝] (-3)⋅ THENA Auto)
         THEN RepUR ``mapfilter`` -1
         THEN (AutoBoolCase ⌜P u⌝⋅ THENA Auto))⋅) }

---

Latex:

---

Latex:
\mforall{}[f1,x:Top].  \mforall{}[T,A:Type].  \mforall{}[as:T  List].  \mforall{}[P:\{a:T|  (a  \mmember{}  as)\}    {}\mrightarrow{}  \mBbbB{}].
\mforall{}[f2:\{a:T|  (a  \mmember{}  as)  \mwedge{}  (\muparrow{}(P  a))\}    {}\mrightarrow{}  A].
    (reduce(f1;x;mapfilter(f2;P;as))  \msim{}  reduce(\mlambda{}u,z.  if  P  u  then  f1  (f2  u)  z  else  z  fi  ;x;as))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  ListInd  (-3)
  THEN  RepUR  ``mapfilter``  0
  THEN  (RepeatFor  2  ((D  0  THENA  Auto))
              THEN  Try  (Trivial)
              THEN  (InstHyp  [\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}f2\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
              THEN  RepUR  ``mapfilter``  -1
              THEN  (AutoBoolCase  \mkleeneopen{}P  u\mkleeneclose{}\mcdot{}  THENA  Auto))\mcdot{})

---

Home Index