Nuprl Definition : OARcast_headers_fun

OARcast_headers_fun(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr) ==
  λhdr.if name_eq(hdr;oarcasthdr) then M
       if name_eq(hdr;orderhdr) then Id × ℤ × M
       if name_eq(hdr;orderedhdr) then Id × Id × ℤ × M
       if name_eq(hdr;deliverhdr) then Id × ℤ × M
       else Top
       fi 


Definitions occuring in Statement :  Id: Id,  name_eq: name_eq(x;y),  ifthenelse: if b then t else f fi ,  top: Top,  lambda: λx.A[x],  product: x:A × B[x],  int: ℤ
FDL editor aliases :  OARcast_headers_fun
Latex:
OARcast\_headers\_fun(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr)  ==
    \mlambda{}hdr.if  name\_eq(hdr;oarcasthdr)  then  M
              if  name\_eq(hdr;orderhdr)  then  Id  \mtimes{}  \mBbbZ{}  \mtimes{}  M
              if  name\_eq(hdr;orderedhdr)  then  Id  \mtimes{}  Id  \mtimes{}  \mBbbZ{}  \mtimes{}  M
              if  name\_eq(hdr;deliverhdr)  then  Id  \mtimes{}  \mBbbZ{}  \mtimes{}  M
              else  Top
              fi 


Date html generated: 2015_07_23-PM-00_28_46
Last ObjectModification: 2014_08_20-AM-11_59_16

Home Index