Nuprl Definition : message-constraint
message-constraint{i:l}(es;X;hdrs;f) == ∀e:E. ((header(e) ∈ hdrs) ⇒ (↓∃e':E. ((e' < e) ∧ <loc(e), info(e)> ∈ X(e'))))
Definitions occuring in Statement :
es-header: header(e),
Message: Message(f),
classrel: v ∈ X(e),
es-info: info(e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
name: Name,
l_member: (x ∈ l),
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]
FDL editor aliases :
message-constraint
Latex:
message-constraint\{i:l\}(es;X;hdrs;f) ==
\mforall{}e:E. ((header(e) \mmember{} hdrs) {}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <loc(e), info(e)> \mmember{} X(e'))))
Date html generated:
2016_05_17-AM-08_55_12
Last ObjectModification:
2014_08_12-AM-11_07_00
Theory : messages
Home
Index