1. the_w : World
2. e : E
3. i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil
4. i:Id, t:. isnull(a(i;t))  (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
5. i:Id, t:, l:IdLnk.
5. isrcv(l;a(i;t))
5. 
5. destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))
6. l:IdLnk, t:.
6. t':. tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil
7. isrcv(kind(e))
8. isrcv(lnk(kind(e));a(loc(e);time(e)))
9. destination(lnk(kind(e))) = loc(e)
10. ||queue(lnk(kind(e));time(e))||1
10. & hd(queue(lnk(kind(e));time(e))) = msg(a(loc(e);time(e)))
11. ||rcvs(lnk(kind(e));time(e))||<||snds(lnk(kind(e));time(e))||
  t:time(e). 
  match(lnk(kind(e));t;time(e))
  & onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||
  & -||snds(lnk(kind(e));t)||)]
  & =
  & msg(a(loc(e);time(e)))
  &  Msg

By:	Unfold `w-queue` -2 THEN ExRepD THEN Thin -3 THEN RWO Thm* m:, L:T List. m<||L||  (nth_tl(m;L) ~ [L[m] / nth_tl(1+m;L)]) -2 THEN Reduce -2

1

10. snds(lnk(kind(e));time(e))[||rcvs(lnk(kind(e));time(e))||] 10. = 10. msg(a(loc(e);time(e))) 10.  Msg 11. ||rcvs(lnk(kind(e));time(e))||<||snds(lnk(kind(e));time(e))||   t:time(e).    match(lnk(kind(e));t;time(e))   & onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))[(||rcvs(lnk(kind(e));time(e))||   & -||snds(lnk(kind(e));t)||)]   & =   & msg(a(loc(e);time(e)))   &  Msg

34 steps

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