---

PropertyN ==
  es:EO+(Info). n:E(New). e:E.
    (e has* New(n)
     (n c e
        (((loc(e) = loc(n)))
          (e':E(Send). ((n <loc e')  e' has* New(n)  (e' < e))))))

---

Definitions :  event-ordering+: EO+(Info),  ses-info: Info,  all: x:A. B[x],  es-E: E,  es-causle: e c e',  implies: P  Q,  not: A,  equal: s = t,  Id: Id,  es-loc: loc(e),  exists: x:A. B[x],  es-E-interface: E(X),  ses-send: Send,  es-locl: (e <loc e'),  and: P  Q,  event-has*: e has* a,  eclass-val: X(e),  ses-new: New,  es-causl: (e < e')
FDL editor aliases :  ses-nonce

---

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: 2010_08_28-AM-02_13_14
Last ObjectModification: 2010_02_22-PM-04_11_14

Home Index