Nuprl Definition : message-constraint2
message-constraint2{i:l}(es;X;hdrs) ==
e1,e2:E.
((es-header(es;e1) 
hdrs)
(es-header(es;e2) hdrs)
single-valued-classrel(es;X;Id 
Message)
(
(e1 = e2))
(
e1',e2':E
((e1' < e1) 
(e2' < e2) ((e1' = e2')) <loc(e1), info(e1)> X(e1') <loc(e2), info(e2)> X(e2'))))
Definitions occuring in Statement :
es-header: es-header(es;e),
Message: Message,
single-valued-classrel: single-valued-classrel(es;X;T),
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],
not: A,
squash: T,
implies: P Q,
and: P Q,
pair: <a, b>,
product: x:A B[x],
equal: s = t,
l_member: (x l)
FDL editor aliases :
message-constraint2
message-constraint2\{i:l\}(es;X;hdrs) ==
\mforall{}e1,e2:E.
((es-header(es;e1) \mmember{} hdrs)
{}\mRightarrow{} (es-header(es;e2) \mmember{} hdrs)
{}\mRightarrow{} single-valued-classrel(es;X;Id \mtimes{} Message)
{}\mRightarrow{} (\mneg{}(e1 = e2))
{}\mRightarrow{} (\mdownarrow{}\mexists{}e1',e2':E
((e1' < e1)
\mwedge{} (e2' < e2)
\mwedge{} (\mneg{}(e1' = e2'))
\mwedge{} <loc(e1), info(e1)> \mmember{} X(e1')
\mwedge{} <loc(e2), info(e2)> \mmember{} X(e2'))))
Date html generated:
2012_01_23-PM-01_12_33
Last ObjectModification:
2011_11_14-AM-00_32_27
Home
Index