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<1
  
  (e,e':E.
  ((z:E. 
  ((e <loc z  isrcv(kind(z)) & e = sender(z)  E
  ((& (z e,e'. e <loc e'  isrcv(kind(e')) & e = sender(e')  E^0 e'))
  (
  (time(e)<time(e'))

None

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