{ 
[T1,T:Type]. (int_consensus_init() 
T List T1 List ) }
{ Proof }
Definitions occuring in Statement :
int_consensus_init: int_consensus_init(),
bool: ,
uall: [x:A]. B[x],
member: t T,
product: x:A B[x],
list: type List,
int: ,
universe: Type
Definitions :
uall: [x:A]. B[x],
member: t T,
int_consensus_init: int_consensus_init()
Lemmas :
bfalse_wf
\mforall{}[T1,T:Type]. (int\_consensus\_init() \mmember{} \mBbbB{} \mtimes{} \mBbbZ{} \mtimes{} T List \mtimes{} T1 List \mtimes{} \mBbbZ{})
Date html generated:
2011_08_16-AM-10_12_20
Last ObjectModification:
2011_06_18-AM-09_04_43
Home
Index