### 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