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: 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