1. the_w : World
2. e : E
3. FairFifo
4. isrcv(kind(e))
5. n : time(e)
6. match(lnk(kind(e));n;time(e))
7. t : 
8. mu(t.match(lnk(kind(e));t;time(e))) = t
  match(lnk(kind(e));t;time(e))
  
  ||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));t)||
   ||onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))||

By:	Analyze 0 THEN RWO 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))|| -1

None

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html