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)
  x.n(x)^d(i;j)(i) = j & (k:. k<d(i;j)  x.n(x)^k(i) = j)

By:	Inst Thm* f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i)) [k.x.n(x)^k+1(i) = j] THENA Trivial THEN Inst Thm* f:(). (n:. f(n))  mu(f)   [k.x.n(x)^k+1(i) = j] THENA Trivial

1

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)

10 steps

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