---

Step * of Lemma es-interval-nil

∀es:EO. ∀e,e':E.  [e, e'] = [] ∈ (E List) ⇐⇒ (e' <loc e) supposing loc(e) = loc(e') ∈ Id
BY
{ Auto  }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. loc(e) = loc(e') ∈ Id
5. [e, e'] = [] ∈ (E List)@i
⊢ (e' <loc e)

2
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)

---

Latex:


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


By

Auto 

---

Home Index