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),  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]],  hdf-invariant: hdf-invariant(A;b.Q[b];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: 2015_07_22-PM-00_00_27
Last ObjectModification: 2014_07_25-PM-02_38_02

Home Index