{ 
s:simple-consensus-state(). v:simple-consensus-msg(). t:
.
(((snd(s)) = 0)
(
isl(v))
(outl(outl(inning_val() <s, v>)) = <0, outl(v)>))
((
isl(v))
((((snd(s)) 
(fst(outr(v))))
(isl(inning_val() <s, v>))
(outl(outl(inning_val() <s, v>)) = outr(v)))
(((fst(outr(v))) = ((snd(s)) - 1))
(||fst(s)|| = (2 * t))
(((x
fst(s).x = (snd(outr(v))))
(isl(outl(inning_val() <s, v>)))
(outr(outl(inning_val() <s, v>)) = (snd(outr(v)))))
((
xfst(s). (x = (snd(outr(v)))))
(isl(inning_val() <s, v>))
(outl(outl(inning_val() <s, v>))
= <snd(s)
, strict-majority-or-max([snd(outr(v)) / (fst(s))])
>))))))
supposing (inning_test(t) s v) }
{ Proof }
Definitions occuring in Statement :
inning_val: inning_val(),
inning_test: inning_test(t),
simple-consensus-msg: simple-consensus-msg(),
simple-consensus-state: simple-consensus-state(),
length: ||as||,
outr: outr(x),
outl: outl(x),
isl: isl(x),
assert: b,
nat: 
,
uimplies: b supposing a,
pi1: fst(t),
pi2: snd(t),
le: A B,
all: x:A. B[x],
not: A,
or: P Q,
and: P Q,
apply: f a,
pair: <a, b>,
product: x:A 
B[x],
cons: [car / cdr],
multiply: n * m,
subtract: n - m,
natural_number: $n,
int: ,
equal: s = t,
l_exists: (xL. P[x]),
l_all: (xL.P[x]),
strict-majority-or-max: strict-majority-or-max(L)
Definitions :
all: x:A. B[x],
uimplies: b supposing a,
assert: b,
or: P Q,
and: P Q,
nat: ,
pi2: snd(t),
isl: isl(x),
outl: outl(x),
inning_val: inning_val(),
not: A,
le: A B,
pi1: fst(t),
outr: outr(x),
member: t T,
implies: P 
Q,
ifthenelse: if b then t else f fi ,
btrue: tt,
bfalse: ff,
true: True,
false: False,
prop: 
,
cand: A c B,
so_lambda: 
x.t[x],
guard: {T},
l_exists: (xL. P[x]),
exists: x:A. B[x],
l_all: (xL.P[x]),
simple-consensus-state: simple-consensus-state(),
simple-consensus-msg: simple-consensus-msg(),
inning_test: inning_test(t),
uall: [x:A]. B[x],
bool: 
,
iff: P 
Q,
so_apply: x[s],
unit: Unit,
decidable: Dec(P),
rev_implies: P Q,
it: 
Lemmas :
assert_witness,
inning_test_wf,
iff_weakening_uiff,
assert_wf,
eq_int_wf,
nat_properties,
assert_of_eq_int,
le_wf,
not_wf,
true_wf,
pi1_wf_top,
nat_wf,
length_wf1,
l_all_wf2,
l_member_wf,
l_exists_wf,
strict-majority-or-max_wf,
simple-consensus-msg_wf,
simple-consensus-state_wf,
bor_wf,
le_int_wf,
band_wf,
decidable__assert,
decidable_wf,
bool_wf,
uiff_transitivity,
eqtt_to_assert,
assert_of_le_int,
false_wf,
lt_int_wf,
bnot_wf,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_le_int,
assert_of_lt_int,
bl-exists_wf,
iff_transitivity,
assert-bl-exists,
assert_of_bnot,
not_functionality_wrt_iff,
assert_of_bor,
or_functionality_wrt_uiff,
assert_of_band,
and_functionality_wrt_uiff,
not_functionality_wrt_uiff,
decidable__equal_int
\mforall{}s:simple-consensus-state(). \mforall{}v:simple-consensus-msg(). \mforall{}t:\mBbbZ{}.
(((snd(s)) = 0) \mwedge{} (\muparrow{}isl(v)) \mwedge{} (outl(outl(inning\_val() <s, v>)) = ɘ, outl(v)>))
\mvee{} ((\mneg{}\muparrow{}isl(v))
\mwedge{} ((((snd(s)) \mleq{} (fst(outr(v))))
\mwedge{} (\muparrow{}isl(inning\_val() <s, v>))
\mwedge{} (outl(outl(inning\_val() <s, v>)) = outr(v)))
\mvee{} (((fst(outr(v))) = ((snd(s)) - 1))
\mwedge{} (||fst(s)|| = (2 * t))
\mwedge{} (((\mforall{}x\mmember{}fst(s).x = (snd(outr(v))))
\mwedge{} (\mneg{}\muparrow{}isl(outl(inning\_val() <s, v>)))
\mwedge{} (outr(outl(inning\_val() <s, v>)) = (snd(outr(v)))))
\mvee{} ((\mexists{}x\mmember{}fst(s). \mneg{}(x = (snd(outr(v)))))
\mwedge{} (\muparrow{}isl(inning\_val() <s, v>))
\mwedge{} (outl(outl(inning\_val() <s, v>))
= <snd(s), strict-majority-or-max([snd(outr(v)) / (fst(s))])>))))))
supposing \muparrow{}(inning\_test(t) s v)
Date html generated:
2011_08_17-PM-06_32_48
Last ObjectModification:
2011_06_18-AM-11_55_55
Home
Index