Nuprl Definition : oar-deliver
Class OARDeliver outputs (i.e. delivers) the
sequenced message ⌈<sndr, n, msg>⌉ at a correct location
only if it has verified that 2*f+1 members of the list
of orderers have signed ⌈<sndr, n, msg>⌉.
Also, it does not deliver ⌈<sndr, n, msg>⌉ unless it has previously
delivered messages ⌈<sndr, n', msg'>⌉ for all n' < n.⋅
oar-deliver(es;M;V;correct;orderers;f;OARDeliver) ==
∀n:ℕ. ∀sndr:Id. ∀msg:M. ∀e:E.
(<sndr, n, msg> ∈ OARDeliver(e)
⇒ (correct loc(e))
⇒ {(0 < n ⇒ (∃msg':M. ∃e':E. ((e' <loc e) ∧ <sndr, n - 1, msg'> ∈ OARDeliver(e))))
∧ (∃L:Id List
((||L|| = ((2 * f) + 1) ∈ ℤ)
∧ no_repeats(Id;L)
∧ (∀o∈L.o ↓∈ orderers ∧ (∃e':E(V). (e' ≤loc e ∧ (∃sig:Atom1. <o, sig, sndr, n, msg> ∈ V(e')))))))})
Definitions occuring in Statement :
es-E-interface: E(X),
classrel: v ∈ X(e),
es-le: e ≤loc e' ,
es-locl: (e <loc e'),
es-loc: loc(e),
es-E: E,
Id: Id,
l_all: (∀x∈L.P[x]),
no_repeats: no_repeats(T;l),
length: ||as||,
list: T List,
nat: ℕ,
atom: Atom$n,
less_than: a < b,
guard: {T},
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
apply: f a,
pair: <a, b>,
product: x:A × B[x],
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T,
bag-member: x ↓∈ bs
FDL editor aliases :
oar-deliver
Latex:
oar-deliver(es;M;V;correct;orderers;f;OARDeliver) ==
\mforall{}n:\mBbbN{}. \mforall{}sndr:Id. \mforall{}msg:M. \mforall{}e:E.
(<sndr, n, msg> \mmember{} OARDeliver(e)
{}\mRightarrow{} (correct loc(e))
{}\mRightarrow{} \{(0 < n {}\mRightarrow{} (\mexists{}msg':M. \mexists{}e':E. ((e' <loc e) \mwedge{} <sndr, n - 1, msg'> \mmember{} OARDeliver(e))))
\mwedge{} (\mexists{}L:Id List
((||L|| = ((2 * f) + 1))
\mwedge{} no\_repeats(Id;L)
\mwedge{} (\mforall{}o\mmember{}L.o \mdownarrow{}\mmember{} orderers
\mwedge{} (\mexists{}e':E(V). (e' \mleq{}loc e \mwedge{} (\mexists{}sig:Atom1. <o, sig, sndr, n, msg> \mmember{} V(e')))))))\})
Date html generated:
2015_07_23-PM-00_26_37
Last ObjectModification:
2014_07_07-PM-01_27_29
Home
Index