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: P ⇒ Q,
and: P ∧ Q,
product: x:A × B[x],
equal: s = 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