---

Step * of Lemma es-base-pred-properties

∀es:EO. ∀e:es-base-E(es).
  ((loc(pred1(e)) = loc(e) ∈ Id)
  ∧ (¬(e < pred1(e)))
  ∧ (∀x:es-base-E(es). ((x < e) ⇒ (loc(x) = loc(e) ∈ Id) ⇒ ((pred1(e) < e) ∧ (¬(pred1(e) < x))))))
BY
{ (InstLemma `event_ordering_properties` []
   THEN ParallelLast
   THEN (ExRepD THENA Auto)
   THEN SplitAndConcl
   THEN Try (BackThruSomeHyp)
   THEN With ⌈e⌉ (D 6)⋅
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}e:es-base-E(es).
    ((loc(pred1(e))  =  loc(e))
    \mwedge{}  (\mneg{}(e  <  pred1(e)))
    \mwedge{}  (\mforall{}x:es-base-E(es).  ((x  <  e)  {}\mRightarrow{}  (loc(x)  =  loc(e))  {}\mRightarrow{}  ((pred1(e)  <  e)  \mwedge{}  (\mneg{}(pred1(e)  <  x))))))


By

(InstLemma  `event\_ordering\_properties`  []
  THEN  ParallelLast
  THEN  (ExRepD  THENA  Auto)
  THEN  SplitAndConcl
  THEN  Try  (BackThruSomeHyp)
  THEN  With  \mkleeneopen{}e\mkleeneclose{}  (D  6)\mcdot{}
  THEN  Auto)

---

Home Index