Nuprl 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))
Proof
Definitions occuring in Statement :
es-rank: es-rank(es;e),
es-locless: es-locless(es;e1;e2),
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,
assert: ↑b,
less_than: a < b,
uimplies: b supposing a,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
Lemmas :
sq_stable__eo_axioms,
event_ordering_wf
\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)))
Date html generated:
2015_07_17-AM-08_34_23
Last ObjectModification:
2015_01_27-PM-02_59_12
Home
Index