---

Step * 3 2 of Lemma l_before-es-interval


1. es : EO@i'
2. e : E@i
3. e' : E@i
4. a : E@i
5. b : E@i
6. (a <loc b)@i
7. e ≤loc a @i
8. b = e' ∈ E@i
⊢ ((a <loc b) ∧ (b <loc e')) ∨ False ∨ ((a <loc e') ∧ (b = e' ∈ E))
BY
{ (OrRight THEN Auto THEN OrRight THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  a  :  E@i
5.  b  :  E@i
6.  (a  <loc  b)@i
7.  e  \mleq{}loc  a  @i
8.  b  =  e'@i
\mvdash{}  ((a  <loc  b)  \mwedge{}  (b  <loc  e'))  \mvee{}  False  \mvee{}  ((a  <loc  e')  \mwedge{}  (b  =  e'))


By

(OrRight  THEN  Auto  THEN  OrRight  THEN  Auto)

---

Home Index