Nuprl Definition : messages-delivered

messages-delivered{i:l}(es;X;f) ==
  ∀e:E. ∀locmsg:Id × Message(f).
    (locmsg ∈ X(e)  (∃e':E. ((e < e') ∧ (loc(e') (fst(locmsg)) ∈ Id) ∧ (info(e') (snd(locmsg)) ∈ Message(f)))))



Definitions occuring in Statement :  Message: Message(f) classrel: v ∈ X(e) es-info: info(e) es-causl: (e < e') es-loc: loc(e) es-E: E Id: Id pi1: fst(t) pi2: snd(t) all: x:A. B[x] exists: x:A. B[x] implies:  Q and: P ∧ Q product: x:A × B[x] equal: t ∈ T
FDL editor aliases :  messages-delivered

Latex:
messages-delivered\{i:l\}(es;X;f)  ==
    \mforall{}e:E.  \mforall{}locmsg:Id  \mtimes{}  Message(f).
        (locmsg  \mmember{}  X(e)  {}\mRightarrow{}  (\mexists{}e':E.  ((e  <  e')  \mwedge{}  (loc(e')  =  (fst(locmsg)))  \mwedge{}  (info(e')  =  (snd(locmsg))))))



Date html generated: 2015_07_21-PM-04_51_06
Last ObjectModification: 2013_02_26-PM-03_12_34

Home Index