Nuprl Definition : base-process-inputs

The base-process-inputs (upto to event e) are the list of m:Info
for which a message ⌈<hdr, loc, m>⌉ has been received ⌈≤loc(e)⌉.
(For this to be well-formed, the header hdr must encode the type
⌈Id × Info⌉). ⋅

base-process-inputs(loc;hdr;es;e) ==
map(λmsg.(snd(msg-body(msg)));filter(λmsg.test-msg-header-and-loc(msg;hdr;loc);map(λe.info(e);≤loc(e))))

Definitions occuring in Statement : test-msg-header-and-loc: test-msg-header-and-loc(msg;hdr;loc), msg-body: msg-body(msg), es-info: info(e), es-le-before: ≤loc(e), filter: filter(P;l), map: map(f;as), pi2: snd(t), lambda: λx.A[x]
FDL editor aliases : base-process-inputs

Latex:
base-process-inputs(loc;hdr;es;e) == map(\mlambda{}msg.(snd(msg-body(msg)));filter(\mlambda{}msg.test-msg-header-and-loc(msg;hdr;loc); map(\mlambda{}e.info(e);\mleq{}loc(e)))) Date html generated: 2015_07_21-PM-04_49_32 Last ObjectModification: 2014_08_06-PM-07_00_11 Home Index