---

Step * 1 of Lemma es-before-partition


1. es : EO
2. e : E
3. e' : E
4. (e' <loc e)
5. ≤loc(e) = (before(e') @ [e', e]) ∈ (E List)
⊢ before(e) = (≤loc(e') @ (e', e)) ∈ (E List)
BY
{ (All (Unfold `es-le-before`)
   THEN (RWW "es-interval-open-interval append_assoc_sq<" (-1) THENA Auto)
   THEN FLemma `general-append-cancellation` [-1]
   THEN Auto) }

---

Latex:



1.  es  :  EO
2.  e  :  E
3.  e'  :  E
4.  (e'  <loc  e)
5.  \mleq{}loc(e)  =  (before(e')  @  [e',  e])
\mvdash{}  before(e)  =  (\mleq{}loc(e')  @  (e',  e))


By

(All  (Unfold  `es-le-before`)
  THEN  (RWW  "es-interval-open-interval  append\_assoc\_sq<"  (-1)  THENA  Auto)
  THEN  FLemma  `general-append-cancellation`  [-1]
  THEN  Auto)

---

Home Index