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

By:	Assert (||snds(lnk(kind(e));t)|| (+||onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))||||snds(lnk(kind(e));t')||)

1

||snds(lnk(kind(e));t)||   +||onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))||||snds(lnk(kind(e));t')||

5 steps

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