Nuprl Definition : hdf-only-headers
hdf-only-headers(f;hdrs;X) == hdf-invariant(Message(f);b.∀mi:Interface. (mi ↓∈ b ⇒ (msg-header(mi.msg) ∈ hdrs));X)
Definitions occuring in Statement :
msg-interface-message: mi.msg,
msg-interface: Interface,
msg-header: msg-header(m),
Message: Message(f),
hdf-invariant: hdf-invariant(A;b.Q[b];X),
name: Name,
l_member: (x ∈ l),
all: ∀x:A. B[x],
implies: P ⇒ Q,
bag-member: x ↓∈ bs
FDL editor aliases :
hdf-only-headers
Latex:
hdf-only-headers(f;hdrs;X) ==
hdf-invariant(Message(f);b.\mforall{}mi:Interface. (mi \mdownarrow{}\mmember{} b {}\mRightarrow{} (msg-header(mi.msg) \mmember{} hdrs));X)
Date html generated:
2016_05_17-AM-09_02_24
Last ObjectModification:
2014_07_16-PM-08_29_16
Theory : messages
Home
Index