Nuprl Definition : strong-message-constraint-no-rep-large
strong-message-constraint-no-rep-large{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))
∧ (∀e':E. ((e' < e) ⇒ (∃e'':E. (e'' ↓∈ bg ∧ e' ≤loc e'' ))))))
Definitions occuring in Statement :
delivered-with-headers: delivered-with-headers(hdrs;es;e),
Message: Message(f),
class-output: class-output(X;es;bg),
es-le: e ≤loc e' ,
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-large
Latex:
strong-message-constraint-no-rep-large\{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))
\mwedge{} (\mforall{}e':E. ((e' < e) {}\mRightarrow{} (\mexists{}e'':E. (e'' \mdownarrow{}\mmember{} bg \mwedge{} e' \mleq{}loc e'' ))))))
Date html generated:
2015_07_21-PM-04_51_33
Last ObjectModification:
2013_02_26-PM-02_30_13
Home
Index