---

Step * of Lemma es-le-not-locl

∀es:EO. ∀e,e':E.  e ≤loc e'  ⇐⇒ ¬(e' <loc e) supposing loc(e) = loc(e') ∈ Id
BY
{ Auto⋅ }

1
1. es : EO@i'
2. e : E@i
3. e' : E@i
4. loc(e) = loc(e') ∈ Id
5. ¬(e' <loc e)@i
⊢ e ≤loc e' 

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}e,e':E.    e  \mleq{}loc  e'    \mLeftarrow{}{}\mRightarrow{}  \mneg{}(e'  <loc  e)  supposing  loc(e)  =  loc(e')


By

---

Latex:
Auto\mcdot{}

---

Home Index