{ nxt_inning() 
simple-consensus-state() 
simple-consensus-msg()
simple-consensus-state() }
{ Proof }
Definitions occuring in Statement :
nxt_inning: nxt_inning(),
simple-consensus-msg: simple-consensus-msg(),
simple-consensus-state: simple-consensus-state(),
member: t T,
function: x:A B[x],
product: x:A B[x]
Definitions :
member: t T,
simple-consensus-state: simple-consensus-state(),
simple-consensus-msg: simple-consensus-msg(),
nxt_inning: nxt_inning(),
nat: 
,
le: A 
B,
not: 
A,
implies: P 
Q,
false: False,
all: 
x:A. B[x],
prop: 
Lemmas :
le_wf,
ifthenelse_wf,
le_int_wf,
nat_properties,
nat_wf
nxt\_inning() \mmember{} simple-consensus-state() \mtimes{} simple-consensus-msg() {}\mrightarrow{} simple-consensus-state()
Date html generated:
2010_08_27-PM-08_30_14
Last ObjectModification:
2010_06_23-PM-11_55_45
Home
Index