Nuprl Definition : class2a
class2a(Op) ==  BaseClass(``paxos 2a``;Id 
 ballot-id() 
 
 
 sm-command(Op))
Proof not projected
Definitions occuring in Statement : 
ballot-id: ballot-id(), 
sm-command: sm-command(Op), 
baseclass: BaseClass(h;T), 
Id: Id, 
product: x:A 
 B[x], 
cons: [car / cdr], 
nil: [], 
int:
, 
token: "$token"
Definitions : 
baseclass: BaseClass(h;T), 
cons: [car / cdr], 
token: "$token", 
nil: [], 
Id: Id, 
ballot-id: ballot-id(), 
product: x:A 
 B[x], 
int:
, 
sm-command: sm-command(Op)
FDL editor aliases : 
class2a
class2a(Op)  ==    BaseClass(``paxos  2a``;Id  \mtimes{}  ballot-id()  \mtimes{}  \mBbbZ{}  \mtimes{}  sm-command(Op))
Date html generated:
2011_10_20-PM-04_17_47
Last ObjectModification:
2011_01_29-AM-00_19_06
Home
Index