Nuprl Definition : ses-NR

PropertyNR ==
  ∀es:EO+(Info). ∀n:E(New). ∀e:E.
    ((loc(e) = loc(n) ∈ Id)
    ⇒ (¬(New(n) released before e))
    ⇒ (∀e':E. ((¬(loc(e') = loc(e) ∈ Id)) ⇒ e' has* New(n) ⇒ (e < e'))))

Definitions occuring in Statement : release-before: (a released before e), event-has*: e has* a, ses-new: New, ses-info: Info, es-E-interface: E(X), eclass-val: X(e), event-ordering+: EO+(Info), es-causl: (e < e'), es-loc: loc(e), es-E: E, Id: Id, all: ∀x:A. B[x], not: ¬A, implies: P ⇒ Q, equal: s = t ∈ T
FDL editor aliases : ses-NR

Latex:
PropertyNR == \mforall{}es:EO+(Info). \mforall{}n:E(New). \mforall{}e:E. ((loc(e) = loc(n)) {}\mRightarrow{} (\mneg{}(New(n) released before e)) {}\mRightarrow{} (\mforall{}e':E. ((\mneg{}(loc(e') = loc(e))) {}\mRightarrow{} e' has* New(n) {}\mRightarrow{} (e < e')))) Date html generated: 2016_05_17-PM-00_24_20 Last ObjectModification: 2012_08_30-PM-04_24_00 Theory : event-logic-applications Home Index