Nuprl Definition : strong-message-constraint
strong-message-constraint{i:l}(es;X;hdrs;f) ==
∀e:E
(↓∃bg:bag(E)
((∀e':E. (e' ↓∈ bg ⇒ (e' < e)))
∧ sub-bag(Id × Message(f);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(f),
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
Latex:
strong-message-constraint\{i:l\}(es;X;hdrs;f) ==
\mforall{}e:E
(\mdownarrow{}\mexists{}bg:bag(E)
((\mforall{}e':E. (e' \mdownarrow{}\mmember{} bg {}\mRightarrow{} (e' < e)))
\mwedge{} sub-bag(Id \mtimes{} Message(f);delivered-with-headers(hdrs;es;e);class-output(X;es;bg))))
Date html generated:
2015_07_21-PM-04_51_23
Last ObjectModification:
2013_02_26-PM-02_34_05
Home
Index