---

Step * 1 of Lemma iseg-es-le-before


1. es : EO@i'
2. e' : E@i
3. e : E@i
4. (e' <loc e)@i
⊢ before(e') @ [e'] ≤ before(e) @ [e]
BY
{ (InstLemma `es-before-decomp` [⌈es⌉;⌈e⌉;⌈e'⌉]⋅ THENA (Auto THEN (BLemma `member-es-before` THEN Auto)⋅)) }

1
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))
⊢ before(e') @ [e'] ≤ before(e) @ [e]

---

Latex:



1.  es  :  EO@i'
2.  e'  :  E@i
3.  e  :  E@i
4.  (e'  <loc  e)@i
\mvdash{}  before(e')  @  [e']  \mleq{}  before(e)  @  [e]


By

(InstLemma  `es-before-decomp`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}
  THENA  (Auto  THEN  (BLemma  `member-es-before`  THEN  Auto)\mcdot{})
  )

---

Home Index