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