the_w:World, e:E, t:.
  FairFifo
  
  isrcv(kind(e))
  
  match(lnk(kind(e));t;time(e))
  
  onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||
  -||snds(lnk(kind(e));t)||)]
  =
  msg(a(loc(e);time(e)))
   Msg

By:	Auto THEN Inst Thm: better-w-match-exists [the_w;e] THEN ExRepD THEN Subst' (t = t1) 0 THEN Inst 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' [the_w;e;t;t1]

None

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