---

Step * 1 1 1 1 of Lemma member-es-interval


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. ev : E@i
5. e ≤loc ev @i
6. ev = e' ∈ E@i
⊢ (ev = e' ∈ E) ∨ False
BY
{ (OrLeft THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  ev  :  E@i
5.  e  \mleq{}loc  ev  @i
6.  ev  =  e'@i
\mvdash{}  (ev  =  e')  \mvee{}  False


By

(OrLeft  THEN  Auto)

---

Home Index