---

Step * of Lemma iseg-es-before

∀es:EO. ∀e',e:E.  ((e' <loc e) ⇒ ≤loc(e') ≤ before(e))
BY
{ (Auto THEN (InstLemma `es-before-decomp` [⌈es⌉;⌈e⌉;⌈e'⌉]⋅ THENA Auto)) }

1
.....antecedent..... 
1. es : EO@i'
2. e' : E@i
3. e : E@i
4. (e' <loc e)@i
⊢ (e' ∈ before(e))

2
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)

---

Latex:


\mforall{}es:EO.  \mforall{}e',e:E.    ((e'  <loc  e)  {}\mRightarrow{}  \mleq{}loc(e')  \mleq{}  before(e))


By

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

---

Home Index