1. the_w : World
2. e : E
3. FairFifo
4. isrcv(kind(e))
5. n:. match(lnk(kind(e));n;time(e))
  sender(e)  E

By:	Inst Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i)) [t.match(lnk(kind(e));t;time(e))] THEN All Reduce THEN Unfold `w-sender` 0 THEN Unfold `w-E` 0 THEN Analyze THEN All Reduce

1

6. match(lnk(kind(e));mu(t.match(lnk(kind(e));t;time(e)));time(e)) 7. i:.  7. i<mu(t.match(lnk(kind(e));t;time(e)))  match(lnk(kind(e));i;time(e))   isnull(a(source(lnk(kind(e)));mu(t.match(lnk(kind(e));t;time(e)))))

4 steps

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