Nuprl Definition : strong-message-constraint
strong-message-constraint{i:l}(es;X;hdrs) ==
e:E
(
bg:bag(E)
((e':E. (e' 
bg 
(e' < e)))
sub-bag(Id 
Message;delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))
Definitions occuring in Statement :
delivered-with-headers: delivered-with-headers(hdrs;es;e),
Message: Message,
class-output: class-output(X;es;bg),
es-causl: (e < e'),
es-E: E,
Id: Id,
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
and: P Q,
product: x:A B[x],
bag-member: x bs,
sub-bag: sub-bag(T;as;bs),
bag: bag(T)
FDL editor aliases :
strong-message-constraint
strong-message-constraint\{i:l\}(es;X;hdrs) ==
\mforall{}e:E
(\mdownarrow{}\mexists{}bg:bag(E)
((\mforall{}e':E. (e' \mdownarrow{}\mmember{} bg {}\mRightarrow{} (e' < e)))
\mwedge{} sub-bag(Id \mtimes{} Message;delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))
Date html generated:
2012_01_23-PM-12_47_22
Last ObjectModification:
2011_11_29-PM-01_17_55
Home
Index