1. n : 
2. R : nnProp
3. x : n
4. y : n
5. n@0 : 
6. j:. j<n@0  (x R^j y)  (k:(n+1). x R^k y)
7. L : n List
8. ||L|| = n@0+1
9. L[0] = x
10. last(L) = y
11. i:n@0. L[i] R L[(i+1)]
12. (i,j:(n@0+1). i<j & L[i] = L[j])
13. a1 : n@0
14. a2 : n@0
15. L[(a1+1)] = L[(a2+1)]
  a1 = a2

1	16. a1<a2   a1 = a2	1 step
2	16. a1<a2   a1 = a2	3 steps

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