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:  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: 2015_07_21-PM-04_51_28
Last ObjectModification: 2013_02_26-PM-02_57_42

Home Index