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: 2016_05_17-PM-00_23_10 Last ObjectModification: 2012_08_30-PM-04_23_21 Theory : event-logic-applications Home Index