---

Step * 1 2 of Lemma loc-ordered-equality


1. es : EO@i'
2. x : E@i
3. y : E@i
4. (x <loc y)@i
5. (y <loc x)@i
6. (x <loc x)
⊢ False
BY
{ (MoveToConcl (-1) THEN Fold `not` 0) }

1
1. es : EO@i'
2. x : E@i
3. y : E@i
4. (x <loc y)@i
5. (y <loc x)@i
⊢ ¬(x <loc x)

---

Latex:



1.  es  :  EO@i'
2.  x  :  E@i
3.  y  :  E@i
4.  (x  <loc  y)@i
5.  (y  <loc  x)@i
6.  (x  <loc  x)
\mvdash{}  False


By

(MoveToConcl  (-1)  THEN  Fold  `not`  0)

---

Home Index