1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i : |R|
5. j : |R|
6. ring(R;in;out)
7. (k.x.n(x)^k+1(i) = j)  
  x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j)  x.n(x)^k(i) = j)

By:	Assert (n:. (k.x.n(x)^k+1(i) = j)(n))

1	n:. (k.x.n(x)^k+1(i) = j)(n)	2 steps
2	8. n:. (k.x.n(x)^k+1(i) = j)(n)   x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j)  x.n(x)^k(i) = j)	11 steps

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