---

Step * 3 of Lemma l_before-es-before-iff


1. the_es : EO@i'
2. e : E@i
3. e' : E@i
4. y : E@i
5. (e' <loc y)@i
6. (y <loc e)@i
⊢ e' before y ∈ before(e)
BY
{ ((RepeatFor 5 ((MoveToConcl (-1))))⋅
   THEN LocLessInd
   THEN Auto
   THEN AssertBY ⌈¬↑first(j)⌉ Auto⋅
   THEN RecUnfold `es-before` 0
   THEN SplitOnConclITE
   THEN Auto) }

1
.....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' <loc y) ⇒ (y <loc k) ⇒ e' before y ∈ before(k))))@i
5. e' : E@i
6. y : E@i
7. (e' <loc y)@i
8. (y <loc j)@i
9. ¬↑first(j)
10. ¬↑first(j)
⊢ e' before y ∈ before(pred(j)) @ [pred(j)]

---

Latex:



1.  the$_{es}$  :  EO@i'
2.  e  :  E@i
3.  e'  :  E@i
4.  y  :  E@i
5.  (e'  <loc  y)@i
6.  (y  <loc  e)@i
\mvdash{}  e'  before  y  \mmember{}  before(e)


By

((RepeatFor  5  ((MoveToConcl  (-1))))\mcdot{}
  THEN  LocLessInd
  THEN  Auto
  THEN  AssertBY  \mkleeneopen{}\mneg{}\muparrow{}first(j)\mkleeneclose{}  Auto\mcdot{}
  THEN  RecUnfold  `es-before`  0
  THEN  SplitOnConclITE
  THEN  Auto)

---

Home Index