1. the_w : World
2. e : E
3. FairFifo
4. isrcv(kind(e))
  index(e)  ||sends(lnk(kind(e));sender(e))||

By:

AssertBY (n:time(e). match(lnk(kind(e));n;time(e))) (BackThru (Thm* the_w:World, e:E. (Thm* FairFifo (Thm*  (Thm* isrcv(kind(e))  (t:time(e). match(lnk(kind(e));t;time(e)))) THEN Inst Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i)) [t.match(lnk(kind(e));t;time(e))] THENA (Reduce 0 THEN ParallelOp -1) THEN Reduce -1 THEN ExRepD

1

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))||

3 steps

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