{ 
[V:Type]
A:Id List. t:
. f:V List 
V. L:consensus-rcv(V;A) List. n:
. v,v2:V.
a:{b:Id| (b 
A)} . i:.
(archive-condition(V;A;t;f;n;v;L @ [Vote[a;i;v2]])
((L = []) 
(i = n) (v = v2))
(((0 < n)
(||values-for-distinct(IdDeq;votes-from-inning(n - 1;L))|| 
(2
* t)))
(
null(filter(
r.n - 1 <z inning(r);L)))
(((i = n) (v = v2))
((((2 * t)
+ 1) ||values-for-distinct(IdDeq;votes-from-inning(n - 1;L
@ [Vote[a;i;v2]]))||)
((f
values-for-distinct(IdDeq;votes-from-inning(n - 1;L
@ [Vote[a;i;v2]])))
= v))))) }
{ Proof }
Definitions occuring in Statement :
archive-condition: archive-condition(V;A;t;f;n;v;L),
votes-from-inning: votes-from-inning(i;L),
rcvd-inning-gt: i <z inning(r),
cs-rcv-vote: Vote[a;i;v],
consensus-rcv: consensus-rcv(V;A),
id-deq: IdDeq,
Id: Id,
length: ||as||,
append: as @ bs,
null: null(as),
assert: b,
nat: ,
uall: [x:A]. B[x],
le: A B,
all: x:A. B[x],
iff: P Q,
or: P Q,
and: P Q,
less_than: a < b,
set: {x:A| B[x]} ,
apply: f a,
lambda: x.A[x],
function: x:A B[x],
cons: [car / cdr],
nil: [],
list: type List,
multiply: n * m,
subtract: n - m,
add: n + m,
natural_number: $n,
int: ,
universe: Type,
equal: s = t,
filter: filter(P;l),
l_member: (x l),
values-for-distinct: values-for-distinct(eq;L)
Definitions :
or: P Q,
and: P Q,
length: ||as||,
guard: {T},
member: t T,
prop: 
,
ycomb: Y,
le: A B,
not: 
A,
implies: P Q,
false: False,
nat: ,
assert: b,
outr: outr(x),
bnot: 
b,
isl: isl(x),
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
true: True,
top: Top,
all: x:A. B[x],
subtype: S 
T,
so_lambda: 
x.t[x],
squash: 
T,
cand: A c B,
archive-condition: archive-condition(V;A;t;f;n;v;L),
exists: 
x:A. B[x],
uall: [x:A]. B[x],
uimplies: b supposing a,
decidable: Dec(P),
hd: hd(l),
tl: tl(l),
consensus-rcv: consensus-rcv(V;A),
cs-rcv-vote: Vote[a;i;v],
cs-initial-rcv: Init[v],
pi1: fst(t),
pi2: snd(t),
so_apply: x[s]
Lemmas :
general-append-cancellation,
consensus-rcv_wf,
cs-rcv-vote_wf,
decidable__equal_int,
length_wf1,
hd_wf,
ge_wf,
tl_wf,
Id_wf,
l_member_wf,
nat_wf,
values-for-distinct_wf,
votes-from-inning_wf,
assert_wf,
null_wf3,
filter_wf_top,
rcvd-inning-gt_wf,
append_wf,
le_wf,
outr_wf,
bnot_wf,
isl_wf,
pi1_wf_top,
pi2_wf,
id-deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self,
nat_properties,
assert_witness,
filter_wf,
top_wf,
bool_wf,
cs-initial-rcv_wf,
squash_wf,
true_wf
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}t:\mBbbN{}. \mforall{}f:V List {}\mrightarrow{} V. \mforall{}L:consensus-rcv(V;A) List. \mforall{}n:\mBbbZ{}. \mforall{}v,v2:V. \mforall{}a:\{b:Id| (b \mmember{} A)\} .
\mforall{}i:\mBbbN{}.
(archive-condition(V;A;t;f;n;v;L @ [Vote[a;i;v2]])
\mLeftarrow{}{}\mRightarrow{} ((L = []) \mwedge{} (i = n) \mwedge{} (v = v2))
\mvee{} (((0 < n) \mwedge{} (||values-for-distinct(IdDeq;votes-from-inning(n - 1;L))|| \mleq{} (2 * t)))
\mwedge{} (\muparrow{}null(filter(\mlambda{}r.n - 1 <z inning(r);L)))
\mwedge{} (((i = n) \mwedge{} (v = v2))
\mvee{} ((((2 * t) + 1) \mleq{} ||values-for-distinct(IdDeq;votes-from-inning(n - 1;L
@ [Vote[a;i;v2]]))||)
\mwedge{} ((f values-for-distinct(IdDeq;votes-from-inning(n - 1;L @ [Vote[a;i;v2]]))) = v)))))
Date html generated:
2011_08_16-AM-10_12_03
Last ObjectModification:
2011_06_18-AM-09_04_27
Home
Index