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. match(lnk(kind(e));mu(t.match(lnk(kind(e));t;time(e)));time(e))
8. i:. 
8. i<mu(t.match(lnk(kind(e));t;time(e)))  match(lnk(kind(e));i;time(e))
  index(e)  ||sends(lnk(kind(e));sender(e))||

By:	Unfold `w-index` 0 THEN Unfolds [`w-sends`;`w-sender`] 0 THEN Reduce 0 THEN Thin -1 THEN MoveToConcl -1 THEN GenConcl (mu(t.match(lnk(kind(e));t;time(e))) = t)

1	n:. (t.match(lnk(kind(e));t;time(e)))(n)	1 step
2	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))||	1 step

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