{ 
[t:
]
(inning_test(t) 
simple-consensus-state() 
simple-consensus-msg() 
) }
{ Proof }
Definitions occuring in Statement :
inning_test: inning_test(t),
simple-consensus-msg: simple-consensus-msg(),
simple-consensus-state: simple-consensus-state(),
bool: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
int:
Definitions :
uall: [x:A]. B[x],
member: t T,
simple-consensus-state: simple-consensus-state(),
simple-consensus-msg: simple-consensus-msg(),
inning_test: inning_test(t),
nat: 
Lemmas :
eq_int_wf,
bor_wf,
le_int_wf,
band_wf,
length_wf1,
nat_wf
\mforall{}[t:\mBbbZ{}]. (inning\_test(t) \mmember{} simple-consensus-state() {}\mrightarrow{} simple-consensus-msg() {}\mrightarrow{} \mBbbB{})
Date html generated:
2011_08_17-PM-06_31_19
Last ObjectModification:
2011_06_18-AM-11_53_54
Home
Index