Nuprl Definition : nysiad_headers_type
nysiad_headers_type{i:l}(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr) ==
{mf:Name ─→ ValueAllType|
nysiad_headers_no_rep(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr)
∧ (∀hdr∈nysiad_headers(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr).(mf hdr)
= (nysiad_headers_fun(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf)
hdr)
∈ Type)}
Definitions occuring in Statement :
nysiad_headers_fun: nysiad_headers_fun(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr;mf),
nysiad_headers_no_rep: nysiad_headers_no_rep(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr),
nysiad_headers: nysiad_headers(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;tooarcasthdr),
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 :
nysiad_headers_type
Latex:
nysiad\_headers\_type\{i:l\}(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;...;...) ==
\{mf:Name {}\mrightarrow{} ValueAllType|
nysiad\_headers\_no\_rep(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;readyhdr;...)
\mwedge{} (\mforall{}hdr\mmember{}nysiad\_headers(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;kdeliverhdr;...;...).
(mf hdr)
= (nysiad\_headers\_fun(add2baghdr;addwaitinghdr;adeliverhdr;inputmsghdr;...;...;...;mf)
hdr))\}
Date html generated:
2015_07_23-PM-03_40_54
Last ObjectModification:
2014_08_06-PM-03_23_20
Home
Index