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:
2016_05_17-PM-03_29_49
Last ObjectModification:
2014_08_06-PM-07_00_11
Theory : messages
Home
Index