is mentioned by

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. 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, i:Id, a:Action(i), l:IdLnk. isrcv(l;a)  msg(a)  Msg	[w-msg_wf]
Thm* the_w:World, l:IdLnk, t:. m(l;t)  Msg List	[w-ml_wf]
Thm* the_w:World, tg:Id, mss:Msg List. w-tagged(tg; mss)  Msg List	[w-tagged_wf]
Thm* the_w:World, l:IdLnk, mss:Msg List. Thm* withlnk(l;mss)  (t:Idthe_w.M(l,t)) List	[w-withlnk_wf]
Thm* the_w:World, l:IdLnk, mss:Msg List. onlnk(l;mss)  Msg List	[w-onlnk_wf]
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)	[fair-fifo]

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