---

Paxos-spec9(es;T;leaders;failset;tg1a;Decide;Input) ==
  f:
   acceptors:Id List
    tg1b,tg2a,tg2b,tgpaxos:Id
     Paxos-spec9-body(es;T;f;acceptors;leaders;...;...;tg1a;...;...;...;...;...)

---

Definitions :  Paxos-spec9-body: Paxos-spec9-body(es;T;f;acceptors;leaders;Input;Decide;...;...;...;...;...;...),  Id: Id,  exists: x:A. B[x],  list: type List,  nat_plus:
FDL editor aliases :  Paxos-spec9

---

Paxos-spec9(es;T;leaders;failset;tg1a;Decide;Input)  ==
    \mexists{}f:\mBbbN{}\msupplus{}
      \mexists{}acceptors:Id  List
        \mexists{}tg1b,tg2a,tg2b,tgpaxos:Id
          Paxos-spec9-body(es;T;f;acceptors;leaders;Input;Decide;tg1a;tg1b;tg2a;tg2b;tgpaxos;failset)


Date html generated: 2010_08_28-PM-01_57_28
Last ObjectModification: 2010_07_15-PM-02_25_34

Home Index