Nuprl Definition : new_23_sig_headers

Nuprl Definition : new_23_sig_headers_fun

new_23_sig_headers_fun(Cmd;notify;propose) ==
  λhdr.if name_eq(hdr;``new_23_sig vote``) then ℤ × ℤ × Cmd × Id
       if name_eq(hdr;``new_23_sig retry``) then ℤ × ℤ × Cmd
       if name_eq(hdr;``new_23_sig decided``) then ℤ × Cmd
       if name_eq(hdr;notify) then ℤ × Cmd
       if name_eq(hdr;propose) then ℤ × Cmd
       else Top
       fi

Definitions occuring in Statement : Id: Id, name_eq: name_eq(x;y), cons: [a / b], nil: [], 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 : new_23_sig_headers_fun

Latex:
new\_23\_sig\_headers\_fun(Cmd;notify;propose) == \mlambda{}hdr.if name\_eq(hdr;``new\_23\_sig vote``) then \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id if name\_eq(hdr;``new\_23\_sig retry``) then \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd if name\_eq(hdr;``new\_23\_sig decided``) then \mBbbZ{} \mtimes{} Cmd if name\_eq(hdr;notify) then \mBbbZ{} \mtimes{} Cmd if name\_eq(hdr;propose) then \mBbbZ{} \mtimes{} Cmd else Top fi Date html generated: 2015_07_23-PM-03_49_37 Last ObjectModification: 2013_11_23-PM-09_54_10 Home Index