---

Step * of Lemma es-causl-locl

∀the_es:EO. ∀e,e':E.  ((e < e') ⇒ (e <loc e') supposing loc(e) = loc(e') ∈ Id)
BY
{ (((((Auto THEN (Inst_ES_Axiom [e; e'] 3)⋅) THENA Auto)
     THEN ThinTrivial
     THEN SplitOrHyps
     THEN Auto
     THEN (InstLemma `es-causal-antireflexive` [the_es; e])⋅)
    THENA Auto
    )
   THEN (D (-1))
   ) }

---

Latex:

---

Latex:
\mforall{}the$_{es}$:EO.  \mforall{}e,e':E.    ((e  <  e')  {}\mRightarrow{}  (e  <loc  e')  supposing  loc(e)  =  loc(e'))


By

---

Latex:
(((((Auto  THEN  (Inst\_ES\_Axiom  [e;  e']  3)\mcdot{})  THENA  Auto)
      THEN  ThinTrivial
      THEN  SplitOrHyps
      THEN  Auto
      THEN  (InstLemma  `es-causal-antireflexive`  [the$_{es}$;  e])\mcdot{})
    THENA  Auto
    )
  THEN  (D  (-1))
  )

---

Home Index