---

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


1. es : EO@i'
2. x : es-base-E(es)@i
3. y : es-base-E(es)@i
4. loc(x) = loc(y) ∈ Id@i
5. (x < y) ⇐⇒ ↑es-locless(es;x;y)
6. (¬↑es-locless(es;x;y)) ⇒ (¬↑es-locless(es;y;x)) ⇒ (x = y ∈ es-base-E(es))
7. es-locless(es;x;y) ∈ 𝔹
8. (x < y) ∈ ℙ
⊢ Dec((x < y))
BY
{ (RWO "-4" 0⋅ THEN Auto) }

---

Latex:



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


By

(RWO  "-4"  0\mcdot{}  THEN  Auto)

---

Home Index