---

Step * 2 of Lemma es-interval-nil


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. loc(e) = loc(e') ∈ Id
5. (e' <loc e)@i
⊢ [e, e'] = [] ∈ (E List)
BY
{ ((RWO "length_zero<" 0 THENA Auto)
   THEN SupposeNot
   THEN AssertBY ⌈e ≤loc e' ⌉ (RWO "es-interval-non-zero" 0 THEN Auto')⋅
   THEN (RWO "es-le-not-locl" (-1))
   THEN Auto) }

---

Latex:



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


By

((RWO  "length\_zero<"  0  THENA  Auto)
  THEN  SupposeNot
  THEN  AssertBY  \mkleeneopen{}e  \mleq{}loc  e'  \mkleeneclose{}  (RWO  "es-interval-non-zero"  0  THEN  Auto')\mcdot{}
  THEN  (RWO  "es-le-not-locl"  (-1))
  THEN  Auto)

---

Home Index