Nuprl Definition : single-valued-on-header
single-valued-on-header{i:l}(Info;X;hdr) == ∀es:EO+(Info). ∀e:E. (↑#([x∈X(e)|name_eq(msg-header(x.msg);hdr)]) ≤z 1)
Definitions occuring in Statement :
msg-interface-message: mi.msg,
msg-header: msg-header(m),
class-ap: X(e),
event-ordering+: EO+(Info),
es-E: E,
name_eq: name_eq(x;y),
le_int: i ≤z j,
assert: ↑b,
all: ∀x:A. B[x],
natural_number: $n,
bag-size: #(bs),
bag-filter: [x∈b|p[x]]
FDL editor aliases :
single-valued-on-header
Latex:
single-valued-on-header\{i:l\}(Info;X;hdr) ==
\mforall{}es:EO+(Info). \mforall{}e:E. (\muparrow{}\#([x\mmember{}X(e)|name\_eq(msg-header(x.msg);hdr)]) \mleq{}z 1)
Date html generated:
2016_05_17-AM-09_01_32
Last ObjectModification:
2014_08_18-PM-01_42_28
Theory : messages
Home
Index