Paxos-spec2{i:l}(Info; es; T; Decide) ==
Reserve:EClass(
)
VoteState:EClass(AcceptorState)
Proposal,Vote:EClass( 
T)
W:Id List List
Paxos-spec2-body{i:l}(Info;es;T;Reserve;VoteState;Proposal;Vote;W;Decide)
Definitions :
paxos-acceptor-state: AcceptorState,
eclass: EClass(A[eo; e]),
product: x:A B[x],
nat: ,
exists: x:A. B[x],
list: type List,
Id: Id,
Paxos-spec2-body: Paxos-spec2-body{i:l}(Info;es;T;Reserve;VoteState;Proposal;Vote;W;Decide)
Paxos-spec2\{i:l\}(Info; es; T; Decide) ==
\mexists{}Reserve:EClass(\mBbbN{})
\mexists{}VoteState:EClass(AcceptorState)
\mexists{}Proposal,Vote:EClass(\mBbbN{} \mtimes{} T)
\mexists{}W:Id List List. Paxos-spec2-body\{i:l\}(Info;es;T;Reserve;VoteState;Proposal;Vote;W;Decide)
Date html generated:
2010_08_28-PM-12_46_48
Last ObjectModification:
2010_04_16-AM-10_55_40
Home
Index