Nuprl Definition : std-ma
StandardMessageAutomaton(X;hdrs) == message-constraint{i:l}(es;X;hdrs;f) ∧ messages-delivered{i:l}(es;X;f)
Definitions occuring in Statement :
message-constraint: message-constraint{i:l}(es;X;hdrs;f),
messages-delivered: messages-delivered{i:l}(es;X;f),
and: P ∧ Q
FDL editor aliases :
std-ma
Latex:
StandardMessageAutomaton(X;hdrs) ==
message-constraint\{i:l\}(es;X;hdrs;f) \mwedge{} messages-delivered\{i:l\}(es;X;f)
Date html generated:
2015_07_21-PM-04_53_02
Last ObjectModification:
2013_02_27-AM-00_53_11
Home
Index