1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i:|R|. 
4. R(source(in(i))) & R(destination(out(i)))
4. & source(out(i)) = i
4. & & destination(in(i)) = i
4. & & in(destination(out(i))) = out(i)
4. & & out(source(in(i))) = in(i)
5. i,j:|R|. k:. x.destination(out(x))^k(i) = j
6. i : |R|
7. k : 
8. x.destination(out(x))^k(i) = i
9. (x.destination(out(x)))  |R||R|
10. i@0 : |R|
11. i@0 = i
12. j:|R|. n:k. x.destination(out(x))^n(i) = j
  y:k. (y  upto(k)) & i@0 = x.destination(out(x))^y(i)  |R|

1	13. n : k 14. x.destination(out(x))^n(i) = i@0  Id   (n  upto(k))	1 step
2	13. n : k 14. x.destination(out(x))^n(i) = i@0  Id   i@0 = x.destination(out(x))^n(i)  |R|	1 step
3	13. n : k 14. x.destination(out(x))^n(i) = i@0  Id 15. y : k 16. (y  upto(k))   x.destination(out(x))^y(i)  |R|	1 step

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