Step
*
2
of Lemma
iseg-es-before
1. es : EO@i'
2. e' : E@i
3. e : E@i
4. (e' <loc e)@i
5. ∃l:E List. (before(e) = (before(e') @ [e'] @ l) ∈ (E List))
⊢ ≤loc(e') ≤ before(e)
BY
{ (ExRepD THEN With ⌜l⌝ (D 0)⋅ THEN Auto) }
1
1. es : EO@i'
2. e' : E@i
3. e : E@i
4. (e' <loc e)@i
5. l : E List
6. before(e) = (before(e') @ [e'] @ l) ∈ (E List)
⊢ before(e) = (≤loc(e') @ l) ∈ (E List)
Latex:
Latex:
1.  es  :  EO@i'
2.  e'  :  E@i
3.  e  :  E@i
4.  (e'  <loc  e)@i
5.  \mexists{}l:E  List.  (before(e)  =  (before(e')  @  [e']  @  l))
\mvdash{}  \mleq{}loc(e')  \mleq{}  before(e)
By
Latex:
(ExRepD  THEN  With  \mkleeneopen{}l\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
Home
Index