1. the_w : World
2. FairFifo
3. e,z:E. e <loc z  isrcv(kind(z)) & e = sender(z)  time(e)<time(z)
4. n : 
5. 0<n
6. 0<n-1
6. 
6. (e,e':E.
6. ((e e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')^n-1 e')
6. (
6. (time(e)<time(e'))
7. n = 1
  0<n
  
  (e,e':E.
  ((e 
  ((if n=0 x,y. x = y  E
  ((else x,y. z:E. 
  ((else x <loc z  isrcv(kind(z)) & x = sender(z)  E
  ((else & (z 
  ((else & (e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n
  ((else & (-1 y) fi e')
  (
  (time(e)<time(e'))

1	8. 0<n 9. n = 0   e,e':E. (e (x,y. x = y  E) e')  time(e)<time(e')	Auto
2	8. 0<n 9. n=0   e,e':E.   (e    ((x,y. z:E.    ((x <loc z  isrcv(kind(z)) & x = sender(z)  E   ((& (z e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^n-1 y)) e')      time(e)<time(e')	1 step

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