{ 
[V:Type]. [A:Id List]. [num:
]. [f:V List 
V]. [s:
{a:Id|
(a 
A)} List
V List
V].
[r:consensus-rcv(V;A)].
(consensus-accum-num(num;f;s;r)
{a:Id| (a A)} List V List V) }
{ Proof }
Definitions occuring in Statement :
consensus-accum-num: consensus-accum-num(num;f;s;r),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
bool: ,
uall: [x:A]. B[x],
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
product: x:A B[x],
list: type List,
int: ,
universe: Type,
l_member: (x l)
Definitions :
uall: [x:A]. B[x],
member: t T,
consensus-accum-num: consensus-accum-num(num;f;s;r),
spreadn: let a,b,c,d,e = u in v[a; b; c; d; e],
spreadn: spread3,
let: let,
so_lambda: 
x.t[x],
consensus-rcv: consensus-rcv(V;A),
prop: 
,
uimplies: b supposing a,
so_apply: x[s],
nat: 
Lemmas :
ifthenelse_wf,
eq_int_wf,
btrue_wf,
bfalse_wf,
consensus-rcv_wf,
bool_wf,
Id_wf,
l_member_wf,
id-deq_wf,
strong-subtype-deq-subtype,
strong-subtype-set3,
strong-subtype-self,
lt_int_wf,
length_wf1,
remove-repeats_wf,
append_wf,
values-for-distinct_wf,
zip_wf
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[num:\mBbbZ{}]. \mforall{}[f:V List {}\mrightarrow{} V]. \mforall{}[s:\mBbbB{} \mtimes{} \mBbbZ{} \mtimes{} \{a:Id| (a \mmember{} A)\} List \mtimes{} V List \mtimes{} V]\000C.
\mforall{}[r:consensus-rcv(V;A)].
(consensus-accum-num(num;f;s;r) \mmember{} \mBbbB{} \mtimes{} \mBbbZ{} \mtimes{} \{a:Id| (a \mmember{} A)\} List \mtimes{} V List \mtimes{} V)
Date html generated:
2011_08_16-AM-10_12_13
Last ObjectModification:
2011_06_18-AM-09_04_35
Home
Index