mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def FairFifo
Def == (i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil  Msg List)
Def == & (i:Id, t:.
Def == & (isnull(a(i;t))
Def == & (
Def == & ((x:Id. s(i;t+1).x = s(i;t).x  vartype(i;x))
Def == & (& m(i;t) = nil  Msg List)
Def == & (i:Id, t:, l:IdLnk.
Def == & (isrcv(l;a(i;t))
Def == & (
Def == & (destination(l) = i
Def == & (& ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))  Msg)
Def == & (l:IdLnk, t:.
Def == & (t':. 
Def == & (tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil  Msg List)

is mentioned by

Thm* i:Id, w:World, p:FairFifo, t:.
Thm* isnull(a(i;t))  (valtype(<i,t>) ~ valtype(i;a(i;t)))		[es-valtype-w-valtype]
Thm* the_w:World. 
Thm* FairFifo
Thm* 
Thm* ESAxioms{i:l}
Thm* ESAxioms(E;
Thm* ESAxioms((i,x. vartype(i;x));
Thm* ESAxioms(the_w.M;
Thm* ESAxioms((e.loc(e));
Thm* ESAxioms((e.kind(e));
Thm* ESAxioms((e.val(e));
Thm* ESAxioms((x,e. (x when e));
Thm* ESAxioms((x,e. (x after e));
Thm* ESAxioms((l,e. sends(l;e));
Thm* ESAxioms((e.sender(e));
Thm* ESAxioms((e.index(e));
Thm* ESAxioms((e.first(e));
Thm* ESAxioms((e.pred(e));
Thm* ESAxioms((e,e'. e <c e'))		[world-event-system]
Thm* the_w:World, e,e':E.
Thm* FairFifo  (e <loc e'  loc(e) = loc(e')  Id & e <c e')		[w-locl-iff]
Thm* the_w:World, e,e':E. FairFifo  e <c e'  time(e)<time(e')[w-causl-time]
Thm* the_w:World, e:E.
Thm* FairFifo  isrcv(kind(e))  index(e)  ||sends(lnk(kind(e));sender(e))||		[w-index_wf]
Thm* the_w:World, e:E. FairFifo  isrcv(kind(e))  sender(e)  E[w-sender_wf]
Thm* the_w:World, e:E, t:.
Thm* FairFifo
Thm* 
Thm* isrcv(kind(e))
Thm* 
Thm* match(lnk(kind(e));t;time(e))
Thm* 
Thm* onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||
Thm* -||snds(lnk(kind(e));t)||)]
Thm* =
Thm* msg(a(loc(e);time(e)))
Thm*  Msg		[w-match-property]
Thm* the_w:World, e:E, t,t':.
Thm* FairFifo
Thm* 
Thm* isrcv(kind(e))
Thm* 
Thm* match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))  t = t'		[w-match-unique]
Thm* the_w:World, e:E.
Thm* FairFifo
Thm* 
Thm* isrcv(kind(e))
Thm* 
Thm* (t:time(e). 
Thm* (match(lnk(kind(e));t;time(e))
Thm* (& onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||
Thm* (& -||snds(lnk(kind(e));t)||)]
Thm* (& =
Thm* (& msg(a(loc(e);time(e)))
Thm* (&  Msg)		[better-w-match-exists]
Thm* the_w:World, e:E.
Thm* FairFifo  isrcv(kind(e))  (t:time(e). match(lnk(kind(e));t;time(e)))		[w-match-exists]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb event system 3 Sections EventSystems Doc