1. the_w : World
2. FairFifo
3. e : E
4. e' : E
5. isrcv(kind(e'))
6. e = sender(e')
7. n : time(e')
8. match(lnk(kind(e'));n;time(e'))
9. match(lnk(kind(e'));mu(t.match(lnk(kind(e'));t;time(e')));time(e'))
10. i:. 
10. i<mu(t.match(lnk(kind(e'));t;time(e')))  match(lnk(kind(e'));i;time(e'))
  time(sender(e'))n

1

11. time(sender(e'))n   n<mu(t.match(lnk(kind(e'));t;time(e')))

2 steps

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