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:
2015_07_23-PM-04_34_17
Last ObjectModification:
2014_11_26-AM-11_31_42
Home
Index