Def match(l;t;t')
Def == (||snds(l;t)||||rcvs(l;t')||)
Def == (||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||)

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, 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]
Thm* the_w:World, l:IdLnk, t,t':. Thm* match(l;t;t') Thm*  Thm* ||snds(l;t)||||rcvs(l;t')|| Thm* & ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||	[assert-w-match]
Def sender(e) == <source(lnk(kind(e))),mu(t.match(lnk(kind(e));t;time(e)))>	[w-sender]

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