---

Step * of Lemma l_before_mapfilter

∀[A,B:Type].
  ∀l:A List. ∀P:A ⟶ 𝔹. ∀f:{a:A| ↑(P a)}  ⟶ B. ∀x,y:B.
    (x before y ∈ mapfilter(f;P;l)
    ⇐⇒ ∃u,v:A. ((↑(P u)) ∧ (↑(P v)) ∧ (x = (f u) ∈ B) ∧ (y = (f v) ∈ B) ∧ u before v ∈ l))
BY
{ (Auto
   THEN All(Unfold `mapfilter`)
   THEN All(RWO "l_before_map")
   THEN Auto
   THEN ExRepD
   THEN (InstConcl [⌜u⌝;⌜v⌝]⋅ THEN Auto)
   THEN Try (Complete (((FLemma `l_before_filter_subtype` [-5] THENA Auto) THEN RWO "l_before_filter" (-1) THEN Auto)))
   THEN Try (Complete (((RWO "l_before_filter_subtype" 0 THENA Auto) THEN BLemma `l_before_filter` THEN Auto)))) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].
    \mforall{}l:A  List.  \mforall{}P:A  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\{a:A|  \muparrow{}(P  a)\}    {}\mrightarrow{}  B.  \mforall{}x,y:B.
        (x  before  y  \mmember{}  mapfilter(f;P;l)
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}u,v:A.  ((\muparrow{}(P  u))  \mwedge{}  (\muparrow{}(P  v))  \mwedge{}  (x  =  (f  u))  \mwedge{}  (y  =  (f  v))  \mwedge{}  u  before  v  \mmember{}  l))


By

---

Latex:
(Auto
  THEN  All(Unfold  `mapfilter`)
  THEN  All(RWO  "l\_before\_map")
  THEN  Auto
  THEN  ExRepD
  THEN  (InstConcl  [\mkleeneopen{}u\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  Try  (Complete  (((FLemma  `l\_before\_filter\_subtype`  [-5]  THENA  Auto)
                                            THEN  RWO  "l\_before\_filter"  (-1)
                                            THEN  Auto)))
  THEN  Try  (Complete  (((RWO  "l\_before\_filter\_subtype"  0  THENA  Auto)
                                            THEN  BLemma  `l\_before\_filter`
                                            THEN  Auto))))

---

Home Index