---

Step * 1 of Lemma es-eq_wf


1. es : EO
⊢ λe1,e2. (loc(e1) = loc(e2) ∧b (¬bes-locless(es;e1;e2)) ∧b (¬bes-locless(es;e2;e1))) ∈ EqDecider(E)
BY
{ ((MemTypeCD THEN Reduce 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
⊢ ¬↑es-locless(es;x;y)

2
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

---

Latex:



1.  es  :  EO
\mvdash{}  \mlambda{}e1,e2.  (loc(e1)  =  loc(e2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;e1;e2))  \mwedge{}\msubb{}  (\mneg{}\msubb{}es-locless(es;e2;e1)))  \mmember{}  EqDecider(E)


By

((MemTypeCD  THEN  Reduce  0)  THEN  Auto)

---

Home Index