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: 2016_05_17-AM-08_52_27
Last ObjectModification: 2014_08_04-PM-03_59_09

Theory : messages


Home Index