---

{ inning_step()  simple-consensus-state()
                   simple-consensus-msg()
                   simple-consensus-state() }

{ Proof }

---

Definitions occuring in Statement :  inning_step: inning_step(),  simple-consensus-msg: simple-consensus-msg(),  simple-consensus-state: simple-consensus-state(),  member: t  T,  function: x:A  B[x]
Definitions :  member: t  T,  simple-consensus-state: simple-consensus-state(),  simple-consensus-msg: simple-consensus-msg(),  inning_step: inning_step(),  nat: ,  all: x:A. B[x]
Lemmas :  ifthenelse_wf,  eq_int_wf,  nat_properties,  nat_wf

---

inning\_step()  \mmember{}  simple-consensus-state()  {}\mrightarrow{}  simple-consensus-msg()  {}\mrightarrow{}  simple-consensus-state()


Date html generated: 2010_08_27-PM-08_30_31
Last ObjectModification: 2010_06_23-PM-11_56_46

Home Index