---

Step * of Lemma decidable__es-causl-same-loc

∀es:EO. ∀x,y:es-base-E(es).  ((loc(x) = loc(y) ∈ Id) ⇒ Dec((x < y)))
BY
{ (InstLemma `es-locless-property` [] THEN RepeatFor 4 (ParallelLast')) }

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)) ∧ ((¬↑es-locless(es;x;y)) ⇒ (¬↑es-locless(es;y;x)) ⇒ (x = y ∈ es-base-E(es)))
⊢ Dec((x < y))

2
.....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 ∈ ℙ

---

Latex:


\mforall{}es:EO.  \mforall{}x,y:es-base-E(es).    ((loc(x)  =  loc(y))  {}\mRightarrow{}  Dec((x  <  y)))


By

(InstLemma  `es-locless-property`  []  THEN  RepeatFor  4  (ParallelLast'))

---

Home Index