{ 
[s:
Id List List ]. (int_consensus_test(s) 
+ Top) }
{ Proof }
Definitions occuring in Statement :
int_consensus_test: int_consensus_test(s),
Id: Id,
bool: ,
uall: [x:A]. B[x],
top: Top,
member: t T,
product: x:A B[x],
union: left + right,
list: type List,
int:
Definitions :
uall: [x:A]. B[x],
member: t T,
top: Top,
int_consensus_test: int_consensus_test(s),
spreadn: let a,b,c,d,e = u in v[a; b; c; d; e]
Lemmas :
ifthenelse_wf,
top_wf,
bool_wf,
Id_wf
\mforall{}[s:\mBbbB{} \mtimes{} \mBbbZ{} \mtimes{} Id List \mtimes{} \mBbbZ{} List \mtimes{} \mBbbZ{}]. (int\_consensus\_test(s) \mmember{} \mBbbZ{} \mtimes{} \mBbbZ{} + Top)
Date html generated:
2011_08_16-AM-10_12_23
Last ObjectModification:
2011_06_18-AM-09_04_47
Home
Index