---

Step * of Lemma l_before-es-before

∀the_es:EO. ∀e,e',y:E.  (e' before y ∈ before(e) ⇒ (e' <loc y))
BY
{ (((LocLessInd THENA Auto) THEN RecUnfold `es-before` 0 THEN SplitOnConclITE) THENA Auto) }

1
.....truecase..... 
1. the_es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e',y:E.  (e' before y ∈ before(k) ⇒ (e' <loc y))))@i
5. ↑first(j)
⊢ ∀e',y:E.  (e' before y ∈ [] ⇒ (e' <loc y))

2
.....falsecase..... 
1. the_es : EO@i'
2. WellFnd{i}(E;x,y.(x <loc y))
3. j : E@i
4. ∀k:E. ((k <loc j) ⇒ (∀e',y:E.  (e' before y ∈ before(k) ⇒ (e' <loc y))))@i
5. ¬↑first(j)
⊢ ∀e',y@0:E.  (e' before y@0 ∈ before(pred(j)) @ [pred(j)] ⇒ (e' <loc y@0))

---

Latex:


\mforall{}the$_{es}$:EO.  \mforall{}e,e',y:E.    (e'  before  y  \mmember{}  before(e)  {}\mRightarrow{}  (e'  <loc  y))


By

(((LocLessInd  THENA  Auto)  THEN  RecUnfold  `es-before`  0  THEN  SplitOnConclITE)  THENA  Auto)

---

Home Index