---

Step * of Lemma es-interval-less

∀[es:EO]. ∀[e,e':E].  [e, e'] = ([e, pred(e')] @ [e']) ∈ (E List) supposing (e <loc e')
BY
{ (Auto THEN Unfold `es-interval` 0 THEN RWO "filter_append" 0 THEN Auto) }

1
1. es : EO
2. e : E
3. e' : E
4. (e <loc e')
⊢ (filter(λev.e ≤loc ev;before(e')) @ filter(λev.e ≤loc ev;[e']))
= ((filter(λev.e ≤loc ev;before(pred(e'))) @ filter(λev.e ≤loc ev;[pred(e')])) @ [e'])
∈ (E List)

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    [e,  e']  =  ([e,  pred(e')]  @  [e'])  supposing  (e  <loc  e')


By

(Auto  THEN  Unfold  `es-interval`  0  THEN  RWO  "filter\_append"  0  THEN  Auto)

---

Home Index