---

Step * of Lemma eo-forward-interval

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[e1,e2,e:E].  ([e1, e2] = [e1, e2] ∈ (E List)) supposing (e1 ≤loc e2  and e ≤loc e1 )
BY
{ ((UnivCD THENA Auto) THEN RepUR ``es-interval`` 0 THEN (RWO "filter_append_sq" 0 THENA Auto) THEN Reduce 0) }

1
1. Info : Type
2. es : EO+(Info)
3. e1 : E
4. e2 : E
5. e : E
6. e ≤loc e1 
7. e1 ≤loc e2 
⊢ (filter(λev.e1 ≤loc ev;before(e2)) @ if e1 ≤loc e2 then [e2] else [] fi )
= (filter(λev.e1 ≤loc ev;before(e2)) @ if e1 ≤loc e2 then [e2] else [] fi )
∈ (E List)

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[e1,e2,e:E].
    ([e1,  e2]  =  [e1,  e2])  supposing  (e1  \mleq{}loc  e2    and  e  \mleq{}loc  e1  )


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``es-interval``  0
  THEN  (RWO  "filter\_append\_sq"  0  THENA  Auto)
  THEN  Reduce  0)

---

Home Index