Nuprl Definition : test-msg-header-and-loc
test-msg-header-and-loc(msg;hdr;loc) == name_eq(msg-header(msg);hdr) ∧b loc = fst(msg-body(msg))
Definitions occuring in Statement :
msg-body: msg-body(msg),
msg-header: msg-header(m),
eq_id: a = b,
name_eq: name_eq(x;y),
band: p ∧b q,
pi1: fst(t)
FDL editor aliases :
test-msg-header-and-loc
Latex:
test-msg-header-and-loc(msg;hdr;loc) == name\_eq(msg-header(msg);hdr) \mwedge{}\msubb{} loc = fst(msg-body(msg))
Date html generated:
2015_07_21-PM-04_49_28
Last ObjectModification:
2014_08_04-PM-03_59_09
Home
Index