Nuprl Definition : strong-message-constraint-bag
strong-message-constraint-bag{i:l}(es; X; hdrs; f) ==
∀be:bag(E)
(bag-no-repeats(E;be)
⇒ (∀e1,e2:E. (e1 ↓∈ be ⇒ e2 ↓∈ be ⇒ (¬(e1 <loc e2))))
⇒ (↓∃bg:bag(E)
(bag-no-repeats(E;bg)
∧ (∀e1,e2:E. (e1 ↓∈ bg ⇒ e2 ↓∈ bg ⇒ (¬(e1 <loc e2))))
∧ (∀e':E. (e' ↓∈ bg ⇒ (∃e:E. (e ↓∈ be ∧ (e' < e)))))
∧ sub-bag(Id × Message(f);∪e∈be.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-combine: ∪x∈bs.f[x],
bag: bag(T)
Latex:
strong-message-constraint-bag\{i:l\}(es; X; hdrs; f) ==
\mforall{}be:bag(E)
(bag-no-repeats(E;be)
{}\mRightarrow{} (\mforall{}e1,e2:E. (e1 \mdownarrow{}\mmember{} be {}\mRightarrow{} e2 \mdownarrow{}\mmember{} be {}\mRightarrow{} (\mneg{}(e1 <loc e2))))
{}\mRightarrow{} (\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{} (\mexists{}e:E. (e \mdownarrow{}\mmember{} be \mwedge{} (e' < e)))))
\mwedge{} sub-bag(Id
\mtimes{} Message(f);\mcup{}e\mmember{}be.delivered-with-headers(hdrs;es;e);class-output(X;es;bg)))))
Date html generated:
2015_07_21-PM-04_52_59
Last ObjectModification:
2013_02_26-PM-03_53_40
Home
Index