---

Step * of Lemma es-locless-property

∀es:EO. ∀x,y:es-base-E(es).
  ((loc(x) = loc(y) ∈ Id)
  ⇒ (((x < y) ⇐⇒ ↑es-locless(es;x;y))
     ∧ ((¬↑es-locless(es;x;y)) ⇒ (¬↑es-locless(es;y;x)) ⇒ (x = y ∈ es-base-E(es)))))
BY
{ (InstLemma `event_ordering_properties` []
   THEN ParallelLast
   THEN SplitAndHyps
   THEN RepeatFor 2 (ParallelLast)
   THEN (InstLemma `es-loc-wf-base` [⌈es⌉;⌈x⌉]⋅ THENA Auto)
   THEN ((InstLemma `es-loc-wf-base` [⌈es⌉;⌈y⌉]⋅ THENA Auto)
         THEN (InstLemma `es-locless-wf-base` [⌈es⌉;⌈x⌉;⌈y⌉]⋅ THENA Auto)
         THEN (InstLemma `es-locless-wf-base` [⌈es⌉;⌈y⌉;⌈x⌉]⋅ THENA Auto)
         THEN (InstLemma `es-causl-wf-base` [⌈es⌉;⌈x⌉;⌈y⌉]⋅ THENA Auto)
         THEN (InstLemma `es-causl-wf-base` [⌈es⌉;⌈y⌉;⌈x⌉]⋅ THENA Auto))
   THEN (D 0 THENA Auto)
   THEN (D -8 THENA Auto)
   THEN Repeat (ParallelLast)
   THEN Auto)⋅ }

---

Latex:


\mforall{}es:EO.  \mforall{}x,y:es-base-E(es).
    ((loc(x)  =  loc(y))
    {}\mRightarrow{}  (((x  <  y)  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}es-locless(es;x;y))
          \mwedge{}  ((\mneg{}\muparrow{}es-locless(es;x;y))  {}\mRightarrow{}  (\mneg{}\muparrow{}es-locless(es;y;x))  {}\mRightarrow{}  (x  =  y))))


By

(InstLemma  `event\_ordering\_properties`  []
  THEN  ParallelLast
  THEN  SplitAndHyps
  THEN  RepeatFor  2  (ParallelLast)
  THEN  (InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ((InstLemma  `es-loc-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `es-locless-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `es-locless-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `es-causl-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `es-causl-wf-base`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  (D  -8  THENA  Auto)
  THEN  Repeat  (ParallelLast)
  THEN  Auto)\mcdot{}

---

Home Index