Paxos-spec8{i:l}(Info; es; T; leader; failset; 1a; Decide; Input) ==
f:
acceptors:Id List
1b:EClass(Id 
(? T))
2a:EClass(Id T)
2b:EClass(Id 
)
Paxos-spec8-body{i:l}(es;
Info;
T;
f;
acceptors;
leader;
Input;
Decide;
1a;
1b;
2a;
2b;
failset)
Definitions :
Paxos-spec8-body: Paxos-spec8-body,
bool: ,
nat: ,
product: x:A B[x],
Id: Id,
eclass: EClass(A[eo; e]),
exists: x:A. B[x],
unit: Unit,
union: left + right,
list: type List,
nat_plus:
Paxos-spec8\{i:l\}(Info; es; T; leader; failset; 1a; Decide; Input) ==
\mexists{}f:\mBbbN{}\msupplus{}
\mexists{}acceptors:Id List
\mexists{}1b:EClass(Id \mtimes{} \mBbbN{} \mtimes{} (?\mBbbN{} \mtimes{} T))
\mexists{}2a:EClass(Id \mtimes{} \mBbbN{} \mtimes{} T)
\mexists{}2b:EClass(Id \mtimes{} \mBbbN{} \mtimes{} \mBbbB{})
Paxos-spec8-body\{i:l\}(es;
Info;
T;
f;
acceptors;
leader;
Input;
Decide;
1a;
1b;
2a;
2b;
failset)
Date html generated:
2010_08_28-PM-01_42_02
Last ObjectModification:
2010_07_15-PM-11_36_45
Home
Index