---

Step * 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)) ∧ ((¬↑es-locless(es;x;y)) ⇒ (¬↑es-locless(es;y;x)) ⇒ (x = y ∈ es-base-E(es)))
⊢ Dec((x < y))
BY
{ D (-1) }

1
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))
⊢ Dec((x < y))

---

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))  \mwedge{}  ((\mneg{}\muparrow{}es-locless(es;x;y))  {}\mRightarrow{}  (\mneg{}\muparrow{}es-locless(es;y;x))  {}\mRightarrow{}  (x  =  y))
\mvdash{}  Dec((x  <  y))


By

D  (-1)

---

Home Index