---

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

---

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

---

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


Date html generated: 2010_08_28-PM-01_59_05
Last ObjectModification: 2010_07_15-PM-02_28_03

Home Index