{ 
[i:
]. (is-vote-from-inning(i) 
simple-consensus-msg() 
) }
{ Proof }
Definitions occuring in Statement :
is-vote-from-inning: is-vote-from-inning(i),
simple-consensus-msg: simple-consensus-msg(),
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-msg: simple-consensus-msg(),
is-vote-from-inning: is-vote-from-inning(i),
band: p 
q,
bnot: 
b,
isl: isl(x),
outr: outr(x),
btrue: tt,
bfalse: ff,
ifthenelse: if b then t else f fi ,
top: Top,
all: x:A. B[x],
subtype: S 
T,
nat: 
Lemmas :
bfalse_wf,
eq_int_wf,
pi1_wf_top,
nat_wf
\mforall{}[i:\mBbbZ{}]. (is-vote-from-inning(i) \mmember{} simple-consensus-msg() {}\mrightarrow{} \mBbbB{})
Date html generated:
2011_08_17-PM-06_32_14
Last ObjectModification:
2011_06_18-AM-11_55_11
Home
Index