1. the_w : World
2. i:Id, t:, l:IdLnk. source(l) = i  onlnk(l;m(i;t)) = nil
3. i:Id, t:. isnull(a(i;t))  (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
4. i:Id, t:, l:IdLnk.
4. isrcv(l;a(i;t))
4. 
4. destination(l) = i & ||queue(l;t)||1 & hd(queue(l;t)) = msg(a(i;t))
5. l:IdLnk, t:.
5. t':. tt' & isrcv(l;a(destination(l);t'))  queue(l;t') = nil
6. e,e':E. loc(e) = loc(e')  e <c e'  e = e'  e' <c e
7. e:E. first(e)  (e':E. loc(e') = loc(e)  e' <c e)
8. e:E. 
8. first(e)
8. 
8. loc(pred(e)) = loc(e) & pred(e) <c e
8. & (e':E. loc(e') = loc(e)  (pred(e) <c e' & e' <c e))
9. e:E. first(e)  (x:Id. (x when e) = (x after pred(e)))
10. Trans e,e':E. e <c e'
11. SWellFounded(e <c e')
12. e:E. 
12. isrcv(kind(e))
12. 
12. sends(lnk(kind(e));sender(e))[index(e)]
12. =
12. msg(lnk(kind(e));tag(kind(e));val(e))
13. e:E. isrcv(kind(e))  sender(e) <c e
14. e,e':E.
14. e <c e'
14. 
14. first(e') & e <c pred(e')  e = pred(e')
14.  isrcv(kind(e')) & e <c sender(e')  e = sender(e')
15. e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))
16. e:E, l:IdLnk. loc(e) = source(l)  sends(l;e) = nil
17. e,e':E.
17. isrcv(kind(e))
17. 
17. isrcv(kind(e'))
17. 
17. lnk(kind(e)) = lnk(kind(e'))
17. 
17. (e <c e'
17. (
17. (sender(e) <c sender(e')  sender(e) = sender(e') & index(e)<index(e'))
18. m : 
19. 0<m
20. l:IdLnk, t:. m-1||snds(l;t)||  (t':. tt' & m-1||rcvs(l;t')||)
21. l : IdLnk
22. t : 
23. m||snds(l;t)||
24. t' : 
25. tt'
26. m-1||rcvs(l;t')||
27. t'@0 : 
28. t't'@0
29. isrcv(l;a(destination(l);t'@0))
  t':. tt' & m||rcvs(l;t')||

1

m||rcvs(l;t'@0+1)||

8 steps

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