Nuprl 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))))))

Proof

Definitions occuring in Statement : es-causl: (e < e'), es-base-pred: pred1(e), es-loc: loc(e), es-base-E: es-base-E(es), event_ordering: EO, Id: Id, all: ∀x:A. B[x], not: ¬A, implies: P ⇒ Q, and: P ∧ Q, equal: s = t ∈ T
Lemmas : event_ordering_properties, es-base-E_wf, event_ordering_wf
\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)))))) Date html generated: 2015_07_17-AM-08_34_24 Last ObjectModification: 2015_01_27-PM-02_59_20 Home Index