{ inning_val() 
simple-consensus-state() 
simple-consensus-msg()
(?
+ ) }
{ Proof }
Definitions occuring in Statement :
inning_val: inning_val(),
simple-consensus-msg: simple-consensus-msg(),
simple-consensus-state: simple-consensus-state(),
nat: ,
unit: Unit,
member: t T,
function: x:A B[x],
product: x:A B[x],
union: left + right,
int:
Definitions :
member: t T,
simple-consensus-state: simple-consensus-state(),
simple-consensus-msg: simple-consensus-msg(),
nat: ,
inning_val: inning_val(),
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
so_lambda: 
x.t[x],
all: 
x:A. B[x],
prop: 
,
so_apply: x[s]
Lemmas :
le_wf,
unit_wf,
ifthenelse_wf,
le_int_wf,
nat_properties,
nat_wf,
bl-exists_wf,
bnot_wf,
eq_int_wf,
l_member_wf,
strict-majority-or-max_wf
inning\_val() \mmember{} simple-consensus-state() \mtimes{} simple-consensus-msg() {}\mrightarrow{} (?\mBbbN{} \mtimes{} \mBbbZ{} + \mBbbZ{})
Date html generated:
2010_08_27-PM-08_30_53
Last ObjectModification:
2010_06_23-PM-11_58_34
Home
Index