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