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 (ParallelLast')) }

1
1. es EO@i'
2. es-base-E(es)@i
3. 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. es-base-E(es)@i
3. 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