---

{ [t:]. [voters,clients:Id List].
    (simple consensus with
     t= t
     voters = voters
     clients = clients  {sys:InitSys| 
                          assuming(env,r.reliable-env(env; r))
                           sys |= es.sc-spec{i:l}(t;voters;clients) es} ) }

{ Proof }

---

Definitions occuring in Statement :  sc-system: sc-system,  sc-spec: sc-spec{i:l}(t;voters;clients),  std-l2m: std-l2m(),  std-n2m: std-n2m(),  strong-realizes: strong-realizes,  InitSys: InitSys,  reliable-env: reliable-env(env; r),  Id: Id,  nat: ,  uall: [x:A]. B[x],  member: t  T,  set: {x:A| B[x]} ,  apply: f a,  list: type List
Definitions :  uall: [x:A]. B[x],  member: t  T,  sc-spec: sc-spec{i:l}(t;voters;clients),  sc-system: sc-system,  uimplies: b supposing a,  all: x:A. B[x]
Lemmas :  comp-system_wf,  sc-compiled_wf,  sc-ok,  Id_wf,  nat_wf

---

\mforall{}[t:\mBbbN{}].  \mforall{}[voters,clients:Id  List].
    (simple  consensus  with
      t=  t
      voters  =  voters
      clients  =  clients  \mmember{}  \{sys:InitSys| 
                                                assuming(env,r.reliable-env(env;  r))
                                                  sys  |=  es.sc-spec\{i:l\}(t;voters;clients)  es\}  )


Date html generated: 2011_08_17-PM-06_35_44
Last ObjectModification: 2011_06_18-AM-11_58_37

Home Index