{ 
[n:
]
(int_consensus_accum(n) 
Id List List
+ (Id )
( Id List List )) }
{ Proof }
Definitions occuring in Statement :
int_consensus_accum: int_consensus_accum(num),
Id: Id,
bool: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
union: left + right,
list: type List,
int:
Definitions :
uall: [x:A]. B[x],
member: t T,
int_consensus_accum: int_consensus_accum(num),
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
Lemmas :
ifthenelse_wf,
eq_int_wf,
btrue_wf,
bfalse_wf,
lt_int_wf,
length_wf1,
remove-repeats_wf,
id-deq_wf,
strict-majority-or-max_wf,
values-for-distinct_wf,
zip_wf,
append_wf,
Id_wf,
bool_wf
\mforall{}[n:\mBbbZ{}]
(int\_consensus\_accum(n) \mmember{} \mBbbB{} \mtimes{} \mBbbZ{} \mtimes{} Id List \mtimes{} \mBbbZ{} List \mtimes{} \mBbbZ{}
{}\mrightarrow{} \mBbbZ{} + (Id \mtimes{} \mBbbZ{} \mtimes{} \mBbbZ{})
{}\mrightarrow{} (\mBbbB{} \mtimes{} \mBbbZ{} \mtimes{} Id List \mtimes{} \mBbbZ{} List \mtimes{} \mBbbZ{}))
Date html generated:
2011_08_16-AM-10_12_16
Last ObjectModification:
2011_06_18-AM-09_04_39
Home
Index