---

Step * 2 of Lemma decidable__es-causl-same-loc

.....wf..... 
1. es : EO@i'
2. x : es-base-E(es)@i
3. y : es-base-E(es)@i
4. (loc(x) = loc(y) ∈ Id)
⇒ (((x < y) ⇐⇒ ↑es-locless(es;x;y)) ∧ ((¬↑es-locless(es;x;y)) ⇒ (¬↑es-locless(es;y;x)) ⇒ (x = y ∈ es-base-E(es))))
⊢ loc(x) = loc(y) ∈ Id ∈ ℙ
BY
{ (InstLemma `es-loc-wf-base` [⌈es⌉]⋅ THEN Auto) }

---

Latex:


.....wf..... 
1.  es  :  EO@i'
2.  x  :  es-base-E(es)@i
3.  y  :  es-base-E(es)@i
4.  (loc(x)  =  loc(y))
{}\mRightarrow{}  (((x  <  y)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}es-locless(es;x;y))
      \mwedge{}  ((\mneg{}\muparrow{}es-locless(es;x;y))  {}\mRightarrow{}  (\mneg{}\muparrow{}es-locless(es;y;x))  {}\mRightarrow{}  (x  =  y)))
\mvdash{}  loc(x)  =  loc(y)  \mmember{}  \mBbbP{}


By

(InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index