---

Step * 1 1 of Lemma es-eq_wf


1. es : EO
2. x : E@i
3. y : E@i
4. x = y ∈ E@i
5. loc(x) = loc(y) ∈ Id
⊢ ¬↑es-locless(es;x;y)
BY
{ (RWO "assert-es-locless" 0 THEN Auto) }

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

---

Latex:



1.  es  :  EO
2.  x  :  E@i
3.  y  :  E@i
4.  x  =  y@i
5.  loc(x)  =  loc(y)
\mvdash{}  \mneg{}\muparrow{}es-locless(es;x;y)


By

(RWO  "assert-es-locless"  0  THEN  Auto)

---

Home Index