Nuprl Definition : message-constraint
message-constraint{i:l}(es;X;hdrs) ==
e:E. ((es-header(es;e) 
hdrs) 
(
e':E. ((e' < e) 
<loc(e), info(e)> X(e'))))
Proof not projected
Definitions occuring in Statement :
es-header: es-header(es;e),
Message: Message,
classrel: v X(e),
es-info: info(e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
name: Name,
all: x:A. B[x],
exists: x:A. B[x],
squash: T,
implies: P Q,
and: P Q,
pair: <a, b>,
product: x:A 
B[x],
l_member: (x l)
FDL editor aliases :
message-constraint
message-constraint\{i:l\}(es;X;hdrs) ==
\mforall{}e:E. ((es-header(es;e) \mmember{} hdrs) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <loc(e), info(e)> \mmember{} X(e'))))
Date html generated:
2011_10_20-PM-03_27_13
Last ObjectModification:
2011_09_02-PM-05_24_41
Home
Index