Nuprl Definition : ses-nonce
PropertyN ==
∀es:EO+(Info). ∀n:E(New). ∀e:E.
(e has* New(n)
⇒ (n c≤ e ∧ ((¬(loc(e) = loc(n) ∈ Id)) ⇒ (∃e':E(Send). ((n <loc e') ∧ e' has* New(n) ∧ (e' < e))))))
Definitions occuring in Statement :
event-has*: e has* a,
ses-send: Send,
ses-new: New,
ses-info: Info,
es-E-interface: E(X),
eclass-val: X(e),
event-ordering+: EO+(Info),
es-causle: e c≤ e',
es-locl: (e <loc e'),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
equal: s = t ∈ T
FDL editor aliases :
ses-nonce
Latex:
PropertyN ==
\mforall{}es:EO+(Info). \mforall{}n:E(New). \mforall{}e:E.
(e has* New(n)
{}\mRightarrow{} (n c\mleq{} e
\mwedge{} ((\mneg{}(loc(e) = loc(n))) {}\mRightarrow{} (\mexists{}e':E(Send). ((n <loc e') \mwedge{} e' has* New(n) \mwedge{} (e' < e))))))
Date html generated:
2015_07_23-PM-00_06_30
Last ObjectModification:
2012_08_30-PM-04_23_21
Home
Index