---

Step * 3 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 ≤loc e' @i
⊢ ((a <loc b) ∧ (b <loc e')) ∨ False ∨ ((a <loc e') ∧ (b = e' ∈ E))
BY
{ D (-1) }

1
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 <loc e')@i
⊢ ((a <loc b) ∧ (b <loc e')) ∨ False ∨ ((a <loc e') ∧ (b = e' ∈ E))

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

---

Latex:

---

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  \mleq{}loc  e'  @i
\mvdash{}  ((a  <loc  b)  \mwedge{}  (b  <loc  e'))  \mvee{}  False  \mvee{}  ((a  <loc  e')  \mwedge{}  (b  =  e'))


By

---

Latex:
D  (-1)

---

Home Index