Nuprl Definition : messages-delivered-with-omissions
messages-delivered-with-omissions{i:l}(es;X;faults;f) ==
∃faulty:bag(Id)
((#(faulty) ≤ faults)
∧ (∀e:E. ∀locmsg:Id × Message(f).
(locmsg ∈ X(e)
⇒ (¬loc(e) ↓∈ faulty)
⇒ (∃e':E. ((e < e') ∧ (loc(e') = (fst(locmsg)) ∈ Id) ∧ (info(e') = (snd(locmsg)) ∈ Message(f)))))))
Definitions occuring in Statement :
Message: Message(f),
classrel: v ∈ X(e),
es-info: info(e),
es-causl: (e < e'),
es-loc: loc(e),
es-E: E,
Id: Id,
pi1: fst(t),
pi2: snd(t),
le: A ≤ B,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
implies: P ⇒ Q,
and: P ∧ Q,
product: x:A × B[x],
equal: s = t ∈ T,
bag-member: x ↓∈ bs,
bag-size: #(bs),
bag: bag(T)
FDL editor aliases :
messages-delivered-with-omissions
Latex:
messages-delivered-with-omissions\{i:l\}(es;X;faults;f) ==
\mexists{}faulty:bag(Id)
((\#(faulty) \mleq{} faults)
\mwedge{} (\mforall{}e:E. \mforall{}locmsg:Id \mtimes{} Message(f).
(locmsg \mmember{} X(e)
{}\mRightarrow{} (\mneg{}loc(e) \mdownarrow{}\mmember{} faulty)
{}\mRightarrow{} (\mexists{}e':E. ((e < e') \mwedge{} (loc(e') = (fst(locmsg))) \mwedge{} (info(e') = (snd(locmsg))))))))
Date html generated:
2016_05_17-AM-08_55_02
Last ObjectModification:
2013_02_26-PM-03_15_28
Theory : messages
Home
Index