---

Step * of Lemma event_ordering_properties

∀eo:EO
  ((∀x,y:es-base-E(eo).  ((x < y) ⇒ es-rank(eo;x) < es-rank(eo;y)))
  ∧ (∀e:es-base-E(eo). (loc(pred1(e)) = loc(e) ∈ Id))
  ∧ (∀e:es-base-E(eo). (¬(e < pred1(e))))
  ∧ (∀e,x:es-base-E(eo).  ((x < e) ⇒ (loc(x) = loc(e) ∈ Id) ⇒ ((pred1(e) < e) ∧ (¬(pred1(e) < x)))))
  ∧ (∀x,y,z:es-base-E(eo).  ((x < y) ⇒ (y < z) ⇒ (x < z)))
  ∧ (∀e1,e2:es-base-E(eo).
       ((e1 < e2) ⇐⇒ ↑es-locless(eo;e1;e2)) ∧ ((¬(e1 < e2)) ⇒ (¬(e2 < e1)) ⇒ (e1 = e2 ∈ es-base-E(eo))) 
       supposing loc(e1) = loc(e2) ∈ Id))
BY
{ ((D 0 THENA Auto)
   THEN (Assert eo_axioms(eo) BY
               (D 1 THEN Unhide THEN Auto))
   THEN Unfold `eo_axioms` -1
   THEN All
   (Folds ``es-causl es-loc es-locless es-base-E es-base-pred es-rank``)⋅
   THEN Trivial) }

---

Latex:


\mforall{}eo:EO
    ((\mforall{}x,y:es-base-E(eo).    ((x  <  y)  {}\mRightarrow{}  es-rank(eo;x)  <  es-rank(eo;y)))
    \mwedge{}  (\mforall{}e:es-base-E(eo).  (loc(pred1(e))  =  loc(e)))
    \mwedge{}  (\mforall{}e:es-base-E(eo).  (\mneg{}(e  <  pred1(e))))
    \mwedge{}  (\mforall{}e,x:es-base-E(eo).    ((x  <  e)  {}\mRightarrow{}  (loc(x)  =  loc(e))  {}\mRightarrow{}  ((pred1(e)  <  e)  \mwedge{}  (\mneg{}(pred1(e)  <  x)))))
    \mwedge{}  (\mforall{}x,y,z:es-base-E(eo).    ((x  <  y)  {}\mRightarrow{}  (y  <  z)  {}\mRightarrow{}  (x  <  z)))
    \mwedge{}  (\mforall{}e1,e2:es-base-E(eo).
              ((e1  <  e2)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}es-locless(eo;e1;e2))  \mwedge{}  ((\mneg{}(e1  <  e2))  {}\mRightarrow{}  (\mneg{}(e2  <  e1))  {}\mRightarrow{}  (e1  =  e2)) 
              supposing  loc(e1)  =  loc(e2)))


By

((D  0  THENA  Auto)
  THEN  (Assert  eo\_axioms(eo)  BY
                          (D  1  THEN  Unhide  THEN  Auto))
  THEN  Unfold  `eo\_axioms`  -1
  THEN  All
  (Folds  ``es-causl  es-loc  es-locless  es-base-E  es-base-pred  es-rank``)\mcdot{}
  THEN  Trivial)

---

Home Index