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))
(
aws.L:consensus-rcv(V;A) List
(L 
s a archive-condition(V;A;t;f;i;v;L))))
Definitions :
no_repeats: no_repeats(T;l),
equal: s = t,
int: ,
length: ||as||,
add: n + m,
multiply: n * m,
natural_number: $n,
l_all: (xL.P[x]),
set: {x:A| B[x]} ,
l_member: (x l),
Id: Id,
exists: x:A. B[x],
list: type List,
and: P Q,
iseg: l1 l2,
consensus-rcv: consensus-rcv(V;A),
apply: f a,
archive-condition: archive-condition(V;A;t;f;n;v;L)
FDL editor aliases :
three-cs-decided
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:
2010_08_27-AM-01_02_03
Last ObjectModification:
2009_12_23-PM-03_34_32
Home
Index