---

Step * 1 1 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, e'] = [] ∈ (E List)@i
6. 0 < ||[e, e']||
⊢ (e' <loc e)
BY
{ ((HypSubst (-2) (-1)) THEN (Reduce (-1)) THEN Auto)⋅ }

---

Latex:



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


By

((HypSubst  (-2)  (-1))  THEN  (Reduce  (-1))  THEN  Auto)\mcdot{}

---

Home Index