{ 
A:Id List. t:
.
(v:
.
s:ts-reachable(three-consensus-ts(;A;t;
L.strict-majority-or-max(L))).
(three-cs-decided(;A;t;L.strict-majority-or-max(L);s;v)
((
a
A. (||s a|| 
1 ) 
(hd(s a) = Init[v]))
(w:.
s':ts-reachable(three-consensus-ts(;A;t;L....)).
((s
(ts-rel(three-consensus-ts(;A;t;...))^*)
s')
three-cs-decided(;A;t;L.strict-majority-or-max(L);s';w)
(v = w)))))) supposing
((||A|| = ((3 * t) + 1)) and
no_repeats(Id;A)) }
{ Proof }
Definitions occuring in Statement :
three-cs-decided: three-cs-decided(V;A;t;f;s;v),
three-consensus-ts: three-consensus-ts(V;A;t;f),
cs-initial-rcv: Init[v],
consensus-rcv: consensus-rcv(V;A),
Id: Id,
hd: hd(l),
length: ||as||,
nat_plus: ,
uimplies: b supposing a,
infix_ap: x f y,
ge: i j ,
all: x:A. B[x],
implies: P Q,
and: P Q,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
list: type List,
multiply: n * m,
add: n + m,
natural_number: $n,
int: ,
equal: s = t,
l_exists: (xL. P[x]),
no_repeats: no_repeats(T;l),
l_member: (x l),
rel_star: R^*,
strict-majority-or-max: strict-majority-or-max(L),
ts-reachable: ts-reachable(ts),
ts-rel: ts-rel(ts),
ts-type: ts-type(ts)
Definitions :
all: x:A. B[x],
uimplies: b supposing a,
implies: P Q,
member: t T,
prop: 
,
nat_plus: ,
eqof: eqof(d),
int-deq: IntDeq,
uall: [x:A]. B[x],
and: P Q,
subtype: S 
T,
guard: {T}
Lemmas :
three-cs-safety,
int-deq_wf,
no_repeats_witness,
Id_wf,
strict-majority-or-max-property,
nat_plus_inc,
strict-majority-or-max_wf,
le_wf,
length_wf1,
filter_wf,
eqof_wf,
ge_wf,
no_repeats_wf,
nat_plus_wf
\mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}.
(\mforall{}v:\mBbbZ{}. \mforall{}s:ts-reachable(three-consensus-ts(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L))).
(three-cs-decided(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L);s;v)
{}\mRightarrow{} ((\mexists{}a\mmember{}A. (||s a|| \mgeq{} 1 ) \mwedge{} (hd(s a) = Init[v]))
\mwedge{} (\mforall{}w:\mBbbZ{}. \mforall{}s':ts-reachable(three-consensus-ts(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L))).
((s
(ts-rel(three-consensus-ts(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L)))\^{}*)
s')
{}\mRightarrow{} three-cs-decided(\mBbbZ{};A;t;\mlambda{}L.strict-majority-or-max(L);s';w)
{}\mRightarrow{} (v = w)))))) supposing
((||A|| = ((3 * t) + 1)) and
no\_repeats(Id;A))
Date html generated:
2011_08_16-AM-10_18_11
Last ObjectModification:
2011_06_18-AM-09_07_18
Home
Index