---

Step * 1 1 of Lemma assert-es-locless


1. es : EO@i'
2. ∀[e:es-base-E(es)]. (loc(e) ∈ Id)
3. x : es-base-E(es)@i
4. y : es-base-E(es)@i
5. loc(x) ∈ Id
6. loc(y) ∈ Id
7. ∀[e,e':es-base-E(es)].  (es-locless(es;e;e') ∈ 𝔹)
8. ∀[e,e':es-base-E(es)].  ((e < e') ∈ ℙ)
9. loc(x) = loc(y) ∈ Id
⊢ ↑es-locless(es;x;y) ⇐⇒ (x < y)
BY
{ (InstLemma `es-locless-property` [⌈es⌉;⌈x⌉;⌈y⌉]⋅ THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  \mforall{}[e:es-base-E(es)].  (loc(e)  \mmember{}  Id)
3.  x  :  es-base-E(es)@i
4.  y  :  es-base-E(es)@i
5.  loc(x)  \mmember{}  Id
6.  loc(y)  \mmember{}  Id
7.  \mforall{}[e,e':es-base-E(es)].    (es-locless(es;e;e')  \mmember{}  \mBbbB{})
8.  \mforall{}[e,e':es-base-E(es)].    ((e  <  e')  \mmember{}  \mBbbP{})
9.  loc(x)  =  loc(y)
\mvdash{}  \muparrow{}es-locless(es;x;y)  \mLeftarrow{}{}\mRightarrow{}  (x  <  y)


By

(InstLemma  `es-locless-property`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index