---

Step * 1 of Lemma es-locl-test


1. es : EO@i'
2. e1 : E@i
3. e2 : E@i
4. (e1 <loc e2)@i
5. (e2 <loc e1)@i
⊢ False
BY
{ Auto }

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index