---

Paxos-spec3{i:l}(Info; es; T; Decide) ==
  f:
   acceptors:Id List
    Reserve:EClass()
     VoteState:EClass(AcceptorState)
      Proposal,Accept:EClass(  T)
       leader:  Id
        Paxos-spec3-body{i:l}(Info;
                              es;
                              T;
                              f;
                              acceptors;
                              Reserve;
                              VoteState;
                              Proposal;
                              Accept;
                              leader;
                              Decide)

---

Definitions :  list: type List,  paxos-acceptor-state: AcceptorState,  eclass: EClass(A[eo; e]),  product: x:A  B[x],  exists: x:A. B[x],  function: x:A  B[x],  nat: ,  Id: Id,  Paxos-spec3-body: Paxos-spec3-body

---

Paxos-spec3\{i:l\}(Info;  es;  T;  Decide)  ==
    \mexists{}f:\mBbbN{}
      \mexists{}acceptors:Id  List
        \mexists{}Reserve:EClass(\mBbbN{})
          \mexists{}VoteState:EClass(AcceptorState)
            \mexists{}Proposal,Accept:EClass(\mBbbN{}  \mtimes{}  T)
              \mexists{}leader:\mBbbN{}  {}\mrightarrow{}  Id
                Paxos-spec3-body\{i:l\}(Info;
                                                            es;
                                                            T;
                                                            f;
                                                            acceptors;
                                                            Reserve;
                                                            VoteState;
                                                            Proposal;
                                                            Accept;
                                                            leader;
                                                            Decide)


Date html generated: 2010_08_28-PM-12_47_09
Last ObjectModification: 2010_04_16-AM-11_48_56

Home Index