---

Step * of Lemma es-pred-exists-between

∀es:EO. ∀e1,e2:E.  ((e1 <loc e2) ⇒ (∃e:{e:E| ¬↑first(e)} . (e1 = pred(e) ∈ E)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN VrCausalInd' THEN Auto THEN UseLoclTri ⌜es⌝⌜e1⌝⌜pred(e2)⌝⋅) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. ∀e':E. ((e' < e2) ⇒ (e1 <loc e') ⇒ (∃e:{e:E| ¬↑first(e)} . (e1 = pred(e) ∈ E)))
5. (e1 <loc e2)@i
6. (e1 <loc pred(e2))
⊢ ∃e:{e:E| ¬↑first(e)} . (e1 = pred(e) ∈ E)

2
1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. ∀e':E. ((e' < e2) ⇒ (e1 <loc e') ⇒ (∃e:{e:E| ¬↑first(e)} . (e1 = pred(e) ∈ E)))
5. (e1 <loc e2)@i
6. (pred(e2) <loc e1)
⊢ ∃e:{e:E| ¬↑first(e)} . (e1 = pred(e) ∈ E)

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}e1,e2:E.    ((e1  <loc  e2)  {}\mRightarrow{}  (\mexists{}e:\{e:E|  \mneg{}\muparrow{}first(e)\}  .  (e1  =  pred(e))))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  VrCausalInd'  THEN  Auto  THEN  UseLoclTri  \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mkleeneopen{}pred(e2)\mkleeneclose{}\mcdot{})

---

Home Index