---

Step * 1 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. e ≤loc a @i
7. e ≤loc b @i
8. ((a <loc b) ∧ (b <loc e')) ∨ False ∨ ((a <loc e') ∧ (b = e' ∈ E))@i
⊢ (a <loc b)
BY
{ (SplitOrHyps THEN Auto THEN Try (((RevHypSubst (-1) (-2)) THEN Auto))) }

---

Latex:



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


By

(SplitOrHyps  THEN  Auto  THEN  Try  (((RevHypSubst  (-1)  (-2))  THEN  Auto)))

---

Home Index