Nuprl Definition : pax-message-types

pax-message-types(Result) ==
  [<pax_p1a(), Id  Ballot_Num()>; 
   
   <pax_p1b(), Id  Ballot_Num()  PVList()>;
    
   <pax_p2a(), Id  PValue()>;
    
   <pax_p2b(), Id  Ballot_Num()>;
    
   <pax_preempted(), Ballot_Num()>;
    
   <pax_adopted(), Ballot_Num()  PVList()>;
    
   <pax_request(), Command()>;
    
   <pax_propose(), Proposal()>; <pax_decision(), Proposal()>; <pax_response(), Cid()  Result>]


Proof not projected



Definitions occuring in Statement :  pax_response: pax_response(),  pax_decision: pax_decision(),  pax_propose: pax_propose(),  pax_request: pax_request(),  pax_adopted: pax_adopted(),  pax_preempted: pax_preempted(),  pax_p2b: pax_p2b(),  pax_p2a: pax_p2a(),  pax_p1b: pax_p1b(),  pax_p1a: pax_p1a(),  PVList: PVList(),  PValue: PValue(),  Proposal: Proposal(),  Command: Command(),  Cid: Cid(),  Ballot_Num: Ballot_Num(),  Id: Id,  pair: <a, b>,  product: x:A  B[x],  cons: [car / cdr],  nil: []
Definitions :  pax_p1a: pax_p1a(),  pax_p1b: pax_p1b(),  pax_p2a: pax_p2a(),  PValue: PValue(),  pax_p2b: pax_p2b(),  Id: Id,  Ballot_Num: Ballot_Num(),  PVList: PVList(),  Command: Command(),  Proposal: Proposal(),  cons: [car / cdr],  pair: <a, b>,  product: x:A  B[x],  Cid: Cid(),  nil: []
FDL editor aliases :  pax-message-types
pax-message-types(Result)  ==
    [<pax\_p1a(),  Id  \mtimes{}  Ballot\_Num()> 
     
      <pax\_p1b(),  Id  \mtimes{}  Ballot\_Num()  \mtimes{}  PVList()>
       
      <pax\_p2a(),  Id  \mtimes{}  PValue()>
       
      <pax\_p2b(),  Id  \mtimes{}  Ballot\_Num()>
       
      <pax\_preempted(),  Ballot\_Num()>
       
      <pax\_adopted(),  Ballot\_Num()  \mtimes{}  PVList()>
       
      <pax\_request(),  Command()>
       
      <pax\_propose(),  Proposal()>  <pax\_decision(),  Proposal()>  <pax\_response(),  Cid()  \mtimes{}  Result>]


Date html generated: 2011_10_20-PM-11_49_13
Last ObjectModification: 2011_05_12-PM-04_56_19

Home Index