{ 
[V:Type]. [A:Id List]. [t:
]. [f:V List 
V]. [v0:V].
[L:consensus-rcv(V;A) List].
(consensus-accum-num-state(t;f;v0;L) 
{a:Id| (a A)} List
V List
V) }
{ Proof }
Definitions occuring in Statement :
consensus-accum-num-state: consensus-accum-num-state(t;f;v0;L),
consensus-rcv: consensus-rcv(V;A),
Id: Id,
bool: ,
nat: ,
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-state: consensus-accum-num-state(t;f;v0;L),
so_lambda: 
x y.t[x; y],
nat: ,
so_apply: x[s1;s2],
prop: 
Lemmas :
list_accum_wf,
bool_wf,
l_member_wf,
bfalse_wf,
consensus-accum-num_wf,
consensus-rcv_wf,
nat_wf,
Id_wf
\mforall{}[V:Type]. \mforall{}[A:Id List]. \mforall{}[t:\mBbbN{}]. \mforall{}[f:V List {}\mrightarrow{} V]. \mforall{}[v0:V]. \mforall{}[L:consensus-rcv(V;A) List].
(consensus-accum-num-state(t;f;v0;L) \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_27
Last ObjectModification:
2011_06_18-AM-09_04_51
Home
Index