Nuprl Definition : strong-message-constraint-bag

strong-message-constraint-bag{i:l}(es; X; hdrs; f) ==
     (∀e1,e2:E.  (e1 ↓∈ be  e2 ↓∈ be  (e1 <loc e2))))
          ∧ (∀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:  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)

strong-message-constraint-bag\{i:l\}(es;  X;  hdrs;  f)  ==
        {}\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)
                    \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