---

Step * 1 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
⊢ ¬(x < y)
BY
{ ((D 0 THEN Auto) THEN InstLemma `es-causal-antireflexive` [⌈es⌉;⌈x⌉]⋅ THEN Auto) }

---

Latex:



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


By

((D  0  THEN  Auto)  THEN  InstLemma  `es-causal-antireflexive`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index