Step * 2 1 of Lemma iseg-es-before


1. es EO@i'
2. e' E@i
3. E@i
4. (e' <loc e)@i
5. List
6. before(e) (before(e') [e'] l) ∈ (E List)
⊢ before(e) (≤loc(e') l) ∈ (E List)
BY
(Unfold `es-le-before` 0  THEN RWO "append_assoc" THEN Auto) }


Latex:


Latex:

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)
\mvdash{}  before(e)  =  (\mleq{}loc(e')  @  l)


By


Latex:
(Unfold  `es-le-before`  0    THEN  RWO  "append\_assoc"  0  THEN  Auto)




Home Index