Nuprl Definition : pv11_p1_headers_no_inputs_types
pv11_p1_headers_no_inputs_types(Cmd) ==
  [<``pv11_p1 p1a``, Id × pv11_p1_Ballot_Num()>
   <``pv11_p1 p1b``, Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)>
   <``pv11_p1 p2a``, Id × pv11_p1_Ballot_Num() × ℤ × Cmd>
   <``pv11_p1 p2b``, Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()>
   <``pv11_p1 preempted``, pv11_p1_Ballot_Num()>
   <``pv11_p1 adopted``, pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)>
   <[decision], ℤ × Cmd>]
Definitions occuring in Statement : 
pv11_p1_Ballot_Num: pv11_p1_Ballot_Num()
, 
Id: Id
, 
cons: [a / b]
, 
nil: []
, 
list: T List
, 
pair: <a, b>
, 
product: x:A × B[x]
, 
int: ℤ
, 
token: "$token"
FDL editor aliases : 
pv11_p1_headers_no_inputs_types
Latex:
pv11\_p1\_headers\_no\_inputs\_types(Cmd)  ==
    [<``pv11\_p1  p1a``,  Id  \mtimes{}  pv11\_p1\_Ballot\_Num()>
      <``pv11\_p1  p1b``
      ,  Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)
      >
      <``pv11\_p1  p2a``,  Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd>
      <``pv11\_p1  p2b``,  Id  \mtimes{}  pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  pv11\_p1\_Ballot\_Num()>
      <``pv11\_p1  preempted``,  pv11\_p1\_Ballot\_Num()>
      <``pv11\_p1  adopted``,  pv11\_p1\_Ballot\_Num()  \mtimes{}  ((pv11\_p1\_Ballot\_Num()  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)  List)>
      <[decision],  \mBbbZ{}  \mtimes{}  Cmd>]
Date html generated:
2016_05_17-PM-02_59_19
Last ObjectModification:
2014_11_26-AM-11_31_42
Theory : paxos!synod
Home
Index