---

Step * 1 2 of Lemma es-eq_wf


1. es : EO
2. x : E@i
3. y : E@i
4. ↑(loc(x) = loc(y) ∧b (¬bes-locless(es;x;y)) ∧b (¬bes-locless(es;y;x)))@i
⊢ x = y ∈ E
BY
{ (RW assert_pushdownC (-1) THEN Auto) }

1
1. es : EO
2. x : E@i
3. y : E@i
4. loc(x) = loc(y) ∈ Id
5. ¬↑es-locless(es;x;y)
6. ¬↑es-locless(es;y;x)
⊢ x = y ∈ E

---

Latex:



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


By

(RW  assert\_pushdownC  (-1)  THEN  Auto)

---

Home Index