---

Step * 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))
⊢ Dec((x < y))
BY
{ ((InstLemma `es-locless-wf-base` [⌈es⌉;⌈x⌉;⌈y⌉]⋅ THENA Auto)
   THEN (InstLemma `es-causl-wf-base` [⌈es⌉;⌈x⌉;⌈y⌉]⋅ THENA Auto)
   ) }

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))
7. es-locless(es;x;y) ∈ 𝔹
8. (x < y) ∈ ℙ
⊢ 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)
6.  (\mneg{}\muparrow{}es-locless(es;x;y))  {}\mRightarrow{}  (\mneg{}\muparrow{}es-locless(es;y;x))  {}\mRightarrow{}  (x  =  y)
\mvdash{}  Dec((x  <  y))


By

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

---

Home Index