Nuprl Definition : has-header-and-in-locs
has-header-and-in-locs(msg;hdr;locs) == name_eq(msg-header(msg);hdr) ∧b bag-deq-member(IdDeq;fst(msg-body(msg));locs)
Definitions occuring in Statement :
msg-body: msg-body(msg),
msg-header: msg-header(m),
id-deq: IdDeq,
name_eq: name_eq(x;y),
band: p ∧b q,
pi1: fst(t),
bag-deq-member: bag-deq-member(eq;x;b)
FDL editor aliases :
has-header-and-in-locs
Latex:
has-header-and-in-locs(msg;hdr;locs) ==
name\_eq(msg-header(msg);hdr) \mwedge{}\msubb{} bag-deq-member(IdDeq;fst(msg-body(msg));locs)
Date html generated:
2015_07_21-PM-04_49_45
Last ObjectModification:
2014_08_05-PM-02_09_36
Home
Index