{ 
[V:Type]
A:Id List. t:
. f:V List 
V. v0:V. L:consensus-rcv(V;A) List.
let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in
archive-condition(V;A;t;f;i - 1;v;L) supposing 
b }
{ Proof }
Definitions occuring in Statement :
consensus-accum-num-state: consensus-accum-num-state(t;f;v0;L),
archive-condition: archive-condition(V;A;t;f;n;v;L),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
assert: b,
nat_plus: ,
spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],
uimplies: b supposing a,
uall: [x:A]. B[x],
all: x:A. B[x],
function: x:A B[x],
list: type List,
subtract: n - m,
natural_number: $n,
universe: Type
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],
uimplies: b supposing a,
prop: 
,
implies: P 
Q,
member: t 
T,
so_lambda: 
x.t[x],
consensus-accum-num-state: consensus-accum-num-state(t;f;v0;L),
assert: b,
list_accum: list_accum(x,a.f[x; a];y;l),
bfalse: ff,
ycomb: Y,
ifthenelse: if b then t else f fi ,
false: False,
and: P 
Q,
length: ||as||,
zip: zip(as;bs),
subtype: S 
T,
top: Top,
consensus-accum-num: consensus-accum-num(num;f;s;r),
btrue: tt,
spreadn: spread3,
let: let,
true: True,
so_lambda: x y.t[x; y],
not: 
A,
guard: {T},
or: P 
Q,
cand: A c B,
values-for-distinct: values-for-distinct(eq;L),
map: map(f;as),
le: A 
B,
cs-rcv-vote: Vote[a;i;v],
filter: filter(P;l),
votes-from-inning: votes-from-inning(i;L),
mapfilter: mapfilter(f;P;L),
rcvd-vote: rcvd-vote(x),
rcvd-inning-eq: inning(r) =
i,
squash: 
T,
outr: outr(x),
band: p 
q,
rcv-vote?: rcv-vote?(x),
reduce: reduce(f;k;as),
Id: Id,
so_apply: x[s],
nat_plus: ,
consensus-rcv: consensus-rcv(V;A),
nat: ,
rev_implies: P 
Q,
iff: P Q,
so_apply: x[s1;s2],
bool: 
,
unit: Unit,
null: null(as),
append: as @ bs,
decidable: Dec(P),
sq_type: SQType(T),
pi1: fst(t),
unzip: unzip(as),
pi2: snd(t),
cs-initial-rcv: Init[v],
it: 
Lemmas :
last_induction,
consensus-rcv_wf,
consensus-accum-num-state_wf,
nat_plus_inc,
bool_wf,
Id_wf,
l_member_wf,
assert_wf,
archive-condition_wf,
nat_plus_wf,
false_wf,
id-deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self,
consensus-accum-num-property1,
append_wf,
top_wf,
eq_int_wf,
true_wf,
filter_wf,
rcvd-inning-gt_wf,
votes-from-inning_wf,
le_wf,
not_wf,
null_wf3,
length_wf1,
values-for-distinct_wf,
zip_wf,
bnot_wf,
archive-condition-append-init,
lt_int_wf,
nat_properties,
archive-condition-append-vote,
le_int_wf,
remove-repeats_wf,
nat_plus_properties,
list_accum_append,
iff_weakening_uiff,
uiff_transitivity,
eqtt_to_assert,
assert_of_eq_int,
eqff_to_assert,
assert_of_bnot,
not_functionality_wrt_uiff,
assert_of_lt_int,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
decidable__assert,
assert_of_null,
filter_wf_top,
member_wf,
subtype_base_sq,
int_subtype_base,
decidable__equal_int,
votes-from-inning-is-nil,
rcvd-innings-nil,
mapfilter-append,
rcvd-inning-eq_wf,
zip-append,
squash_wf,
length_wf_nat,
nat_wf,
length-map,
map_wf,
pi1_wf_top,
length-append,
unzip_zip,
pi2_wf,
list_subtype_base,
set_subtype_base,
atom2_subtype_base
\mforall{}[V:Type]
\mforall{}A:Id List. \mforall{}t:\mBbbN{}\msupplus{}. \mforall{}f:V List {}\mrightarrow{} V. \mforall{}v0:V. \mforall{}L:consensus-rcv(V;A) List.
let b,i,as,vs,v = consensus-accum-num-state(t;f;v0;L) in archive-condition(V;A;t;f;i - 1;v;L)
supposing \muparrow{}b
Date html generated:
2011_08_16-AM-10_14_17
Last ObjectModification:
2011_06_18-AM-09_06_29
Home
Index