{ 
[L:simple-consensus-msg() List]. [s:simple-consensus-state()].
(snd(list_accum(s,v.inning_step() s v;s;L)) ~ snd(s)) }
{ Proof }
Definitions occuring in Statement :
inning_step: inning_step(),
simple-consensus-msg: simple-consensus-msg(),
simple-consensus-state: simple-consensus-state(),
uall: [x:A]. B[x],
pi2: snd(t),
apply: f a,
list: type List,
sqequal: s ~ t,
list_accum: list_accum(x,a.f[x; a];y;l)
Definitions :
uall: [x:A]. B[x],
pi2: snd(t),
member: t 
T
Lemmas :
inning_steps,
simple-consensus-state_wf,
simple-consensus-msg_wf
\mforall{}[L:simple-consensus-msg() List]. \mforall{}[s:simple-consensus-state()].
(snd(list\_accum(s,v.inning\_step() s v;s;L)) \msim{} snd(s))
Date html generated:
2011_08_17-PM-06_32_34
Last ObjectModification:
2011_06_18-AM-11_55_40
Home
Index