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)  
8. n:. (k.x.n(x)^k+1(i) = j)(n)
9. (k.x.n(x)^k+1(i) = j)(mu(k.x.n(x)^k+1(i) = j))
9. & (i@0:. i@0<mu(k.x.n(x)^k+1(i) = j)  (k.x.n(x)^k+1(i) = j)(i@0))
10. mu(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:	All Reduce THEN Subst (mu(k.x.n(x)^k+1(i) = j) ~ (d(i;j)-1)) -2

1	8. n:. x.n(x)^n+1(i) = j 9. x.n(x)^mu(k.x.n(x)^k+1(i) = j)+1(i) = j 9. & (i@0:. i@0<mu(k.x.n(x)^k+1(i) = j)  x.n(x)^i@0+1(i) = j) 10. mu(k.x.n(x)^k+1(i) = j)     mu(k.x.n(x)^k+1(i) = j) ~ (d(i;j)-1)	1 step
2	8. n:. x.n(x)^n+1(i) = j 9. x.n(x)^d(i;j)-1+1(i) = j & (i@0:. i@0<d(i;j)-1  x.n(x)^i@0+1(i) = j) 10. mu(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)	8 steps

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