mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
RankTheoremName
5Thm* 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]
cites the following:
4Thm* 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]
3Thm* 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]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
mb event system 3 Sections EventSystems Doc