Nuprl Definition : strong-message-constraint-no-rep
strong-message-constraint-no-rep{i:l}(es;X;hdrs;f) ==
∀e:E
(↓∃bg:bag(E)
(bag-no-repeats(E;bg)
∧ (∀e1,e2:E. (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2))))
∧ (∀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-locl: (e <loc e'),
es-causl: (e < e'),
es-E: E,
Id: Id,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
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-no-repeats: bag-no-repeats(T;bs),
bag: bag(T)
FDL editor aliases :
strong-message-constraint-no-rep
Latex:
strong-message-constraint-no-rep\{i:l\}(es;X;hdrs;f) ==
\mforall{}e:E
(\mdownarrow{}\mexists{}bg:bag(E)
(bag-no-repeats(E;bg)
\mwedge{} (\mforall{}e1,e2:E. (e1 \mdownarrow{}\mmember{} bg {}\mRightarrow{} e2 \mdownarrow{}\mmember{} bg {}\mRightarrow{} (\mneg{}(e1 <loc e2))))
\mwedge{} (\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:
2016_05_17-AM-08_55_37
Last ObjectModification:
2013_02_26-PM-02_57_42
Theory : messages
Home
Index