---

Step * of Lemma member-es-before

∀the_es:EO. ∀e',e:E.  ((e ∈ before(e')) ⇐⇒ (e <loc e'))
BY
{ (((((LocLessInd THENA Auto) THEN D 0) 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:E. ((e ∈ before(k)) ⇐⇒ (e <loc k))))@i
5. e : E@i
6. ↑first(j)
⊢ (e ∈ []) ⇐⇒ (e <loc j)

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

---

Latex:


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


By

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

---

Home Index