Nuprl Definition : pv11_p1_headers

Nuprl Definition : pv11_p1_headers_fun

pv11_p1_headers_fun(Cmd) ==
λhdr.if name_eq(hdr;``pv11_p1 p1a``) then Id × pv11_p1_Ballot_Num()
if name_eq(hdr;``pv11_p1 p1b``)

         then Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)

       if name_eq(hdr;``pv11_p1 p2a``) then Id × pv11_p1_Ballot_Num() × ℤ × Cmd
       if name_eq(hdr;``pv11_p1 p2b``) then Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()
       if name_eq(hdr;``pv11_p1 preempted``) then pv11_p1_Ballot_Num()

       if name_eq(hdr;``pv11_p1 adopted``) then pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)

       if name_eq(hdr;[propose]) then ℤ × Cmd
       if name_eq(hdr;[decision]) then ℤ × Cmd
       else Top
       fi

Definitions occuring in Statement : pv11_p1_Ballot_Num: pv11_p1_Ballot_Num(), Id: Id, name_eq: name_eq(x;y), cons: [a / b], nil: [], list: T List, ifthenelse: if b then t else f fi , top: Top, lambda: λx.A[x], product: x:A × B[x], int: ℤ, token: "$token"
FDL editor aliases : pv11_p1_headers_fun

Latex:
pv11\_p1\_headers\_fun(Cmd) == \mlambda{}hdr.if name\_eq(hdr;``pv11\_p1 p1a``) then Id \mtimes{} pv11\_p1\_Ballot\_Num() if name\_eq(hdr;``pv11\_p1 p1b``) then Id \mtimes{} pv11\_p1\_Ballot\_Num() \mtimes{} pv11\_p1\_Ballot\_Num() \mtimes{} ((pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List) if name\_eq(hdr;``pv11\_p1 p2a``) then Id \mtimes{} pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd if name\_eq(hdr;``pv11\_p1 p2b``) then Id \mtimes{} pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} pv11\_p1\_Ballot\_Num() if name\_eq(hdr;``pv11\_p1 preempted``) then pv11\_p1\_Ballot\_Num() if name\_eq(hdr;``pv11\_p1 adopted``) then pv11\_p1\_Ballot\_Num() \mtimes{} ((pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbZ{} \mtimes{} Cmd) List) if name\_eq(hdr;[propose]) then \mBbbZ{} \mtimes{} Cmd if name\_eq(hdr;[decision]) then \mBbbZ{} \mtimes{} Cmd else Top fi Date html generated: 2015_07_23-PM-04_11_09 Last ObjectModification: 2014_11_26-AM-11_22_28 Home Index