Nuprl Definition : hdf-single-valued-except
A halting-dataflow from ⌜Message(f)⌝ to ⌜Interface⌝ is single valued
except on a list of headers if after processing any list L of messages
it is either halted or else, after filtering out the part of the output
with the given headers, what remains is a single-valued bag.⋅
hdf-single-valued-except(f;hdrs;X) ==
  hdf-invariant(Message(f);b.single-valued-bag([x∈b|¬bmsg-header(snd(snd(x))) ∈b hdrs];Interface);X)
Definitions occuring in Statement : 
msg-interface: Interface
, 
msg-header: msg-header(m)
, 
Message: Message(f)
, 
hdf-invariant: hdf-invariant(A;b.Q[b];X)
, 
name-deq: NameDeq
, 
deq-member: x ∈b L
, 
bnot: ¬bb
, 
pi2: snd(t)
, 
single-valued-bag: single-valued-bag(b;T)
, 
bag-filter: [x∈b|p[x]]
FDL editor aliases : 
hdf-single-valued-except
Latex:
hdf-single-valued-except(f;hdrs;X)  ==
    hdf-invariant(Message(f);b.single-valued-bag([x\mmember{}b|\mneg{}\msubb{}msg-header(snd(snd(x)))  \mmember{}\msubb{}  hdrs];Interface);X)
Date html generated:
2016_05_17-PM-03_30_04
Last ObjectModification:
2014_07_25-PM-02_38_02
Theory : messages
Home
Index