messages-delivered{i:l}(es;X) ==
e:E. locmsg:Id 
Message.
(locmsg 
X(e)
(
e':E
((e < e') 
(loc(e') = (fst(locmsg))) (info(e') = (snd(locmsg))))))
Definitions occuring in Statement :
Message: Message,
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
Definitions :
all: x:A. B[x],
implies: P Q,
classrel: v X(e),
product: x:A B[x],
exists: x:A. B[x],
es-E: E,
es-causl: (e < e'),
and: P Q,
Id: Id,
es-loc: loc(e),
pi1: fst(t),
equal: s = t,
Message: Message,
es-info: info(e),
pi2: snd(t)
FDL editor aliases :
messages-delivered
messages-delivered\{i:l\}(es;X) ==
\mforall{}e:E. \mforall{}locmsg:Id \mtimes{} Message.
(locmsg \mmember{} X(e) {}\mRightarrow{} (\mexists{}e':E. ((e < e') \mwedge{} (loc(e') = (fst(locmsg))) \mwedge{} (info(e') = (snd(locmsg))))))
Date html generated:
2011_08_17-PM-04_05_58
Last ObjectModification:
2011_05_23-PM-05_23_03
Home
Index