the_w:World, e:E, t,t':.
  FairFifo
  
  isrcv(kind(e))
  
  t<t'  match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))

By:	Auto THEN Analyze 0 THEN All (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))||) THEN ExRepD

1

1. the_w : World 2. e : E 3. t :  4. t' :  5. FairFifo 6. isrcv(kind(e)) 7. t<t' 8. ||snds(lnk(kind(e));t)||||rcvs(lnk(kind(e));time(e))|| 9. ||rcvs(lnk(kind(e));time(e))||<||snds(lnk(kind(e));t)|| 9. +||onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))|| 10. ||snds(lnk(kind(e));t')||||rcvs(lnk(kind(e));time(e))|| 11. ||rcvs(lnk(kind(e));time(e))||<||snds(lnk(kind(e));t')|| 11. +||onlnk(lnk(kind(e));m(source(lnk(kind(e)));t'))||   False

6 steps

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