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. r : 
11. ||rcvs(lnk(kind(e));time(e))|| = r
12. ms : Msg
13. msg(a(loc(e);time(e))) = ms
14. l : IdLnk
15. lnk(kind(e)) = l
16. t' : 
17. time(e) = t'
18. r<||snds(l;t')||
19. concat(map(t1.m(l;t1);upto(t')))[r] = ms
20. m : ||map(t1.m(l;t1);upto(t'))||
21. ||concat(firstn(m;map(t1.m(l;t1);upto(t'))))||r
21. & r-||concat(firstn(m;map(t1.m(l;t1);upto(t'))))||<||map(t1.
21. m(l;t1);upto(t'))[m]||
21. & concat(map(t1.m(l;t1);upto(t')))[r]
21. & =
21. & map(t1.m(l;t1);upto(t'))[m][(r-||concat(firstn(m;map(t1.
21. & m(l;t1);upto(t'))))||)]
22. m<t'
  t:t'. 
  ((||snds(l;t)||r)(r<||snds(l;t)||+||onlnk(l;m(source(l);t))||))
  & onlnk(l;m(source(l);t))[(r-||snds(l;t)||)] = ms  Msg

By:	RWO Thm* f:(TopTop), n:, l:Top List. firstn(n;map(f;l)) ~ map(f;firstn(n;l)) -2 THEN RWO Thm* n,m:. firstn(n;upto(m)) ~ if nm upto(n) else upto(m) fi -2 THEN Subst ((mt') ~ true) -2 THEN Try (Complete (AutoBoolCase (mt'))) THEN Reduce -2 THEN Fold `w-snds` -2 THEN ExRepD

1

21. ||snds(l;m)||r 22. r-||snds(l;m)||<||map(t1.m(l;t1);upto(t'))[m]|| 23. snds(l;t')[r] = map(t1.m(l;t1);upto(t'))[m][(r-||snds(l;m)||)]  Msg 24. m<t'   t:t'.    ((||snds(l;t)||r)(r<||snds(l;t)||+||onlnk(l;m(source(l);t))||))   & onlnk(l;m(source(l);t))[(r-||snds(l;t)||)] = ms  Msg

24 steps

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