Nuprl Definition : OARcast_headers

Nuprl Definition : OARcast_headers_type

OARcast_headers_type{i:l}(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr) ==
  {mf:Name ─→ ValueAllType|
   OARcast_headers_no_rep(deliverhdr;oarcasthdr;orderedhdr;orderhdr)
   ∧ (∀hdr∈OARcast_headers(deliverhdr;oarcasthdr;orderedhdr;orderhdr).(mf hdr)
          = (OARcast_headers_fun(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr) hdr)
          ∈ Type)}

Definitions occuring in Statement : OARcast_headers_fun: OARcast_headers_fun(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr), OARcast_headers_no_rep: OARcast_headers_no_rep(deliverhdr;oarcasthdr;orderedhdr;orderhdr), OARcast_headers: OARcast_headers(deliverhdr;oarcasthdr;orderedhdr;orderhdr), name: Name, l_all: (∀x∈L.P[x]), vatype: ValueAllType, and: P ∧ Q, set: {x:A| B[x]} , apply: f a, function: x:A ─→ B[x], universe: Type, equal: s = t ∈ T
FDL editor aliases : OARcast_headers_type

Latex:
OARcast\_headers\_type\{i:l\}(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr) == \{mf:Name {}\mrightarrow{} ValueAllType| OARcast\_headers\_no\_rep(deliverhdr;oarcasthdr;orderedhdr;orderhdr) \mwedge{} (\mforall{}hdr\mmember{}OARcast\_headers(deliverhdr;oarcasthdr;orderedhdr;orderhdr).(mf hdr) = (OARcast\_headers\_fun(M;deliverhdr;oarcasthdr;orderedhdr;orderhdr) hdr))\} Date html generated: 2015_07_23-PM-00_28_53 Last ObjectModification: 2014_08_20-AM-11_59_29 Home Index