Nuprl Definition : three-cs-decided
three-cs-decided(V;A;t;f;s;v) ==
∃i:ℤ
∃ws:{a:Id| (a ∈ A)} List
(no_repeats({a:Id| (a ∈ A)} ;ws)
∧ (||ws|| = ((2 * t) + 1) ∈ ℤ)
∧ (∀a∈ws.∃L:consensus-rcv(V;A) List. (L ≤ s a ∧ archive-condition(V;A;t;f;i;v;L))))
Definitions occuring in Statement :
archive-condition: archive-condition(V;A;t;f;n;v;L),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
iseg: l1 ≤ l2,
l_all: (∀x∈L.P[x]),
no_repeats: no_repeats(T;l),
l_member: (x ∈ l),
length: ||as||,
list: T List,
exists: ∃x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
multiply: n * m,
add: n + m,
natural_number: $n,
int: ℤ,
equal: s = t ∈ T
FDL editor aliases :
three-cs-decided
Latex:
three-cs-decided(V;A;t;f;s;v) ==
\mexists{}i:\mBbbZ{}
\mexists{}ws:\{a:Id| (a \mmember{} A)\} List
(no\_repeats(\{a:Id| (a \mmember{} A)\} ;ws)
\mwedge{} (||ws|| = ((2 * t) + 1))
\mwedge{} (\mforall{}a\mmember{}ws.\mexists{}L:consensus-rcv(V;A) List. (L \mleq{} s a \mwedge{} archive-condition(V;A;t;f;i;v;L))))
Date html generated:
2016_05_16-PM-00_44_25
Last ObjectModification:
2012_07_09-PM-06_26_01
Theory : event-ordering
Home
Index