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

By:	Subst ((d(i;p(j))+1) ~ (1+d(i;p(j)))) 0 THENL [Auto;Id] THEN Inst Thm* n,m:, f:(TT). f^n+m = f^n o f^m [|R|;1;d(i;p(j));x.n(x)] THEN HypSubst -1 0 THEN Reduce 0

1

13. x.n(x)^1+d(i;p(j)) = x.n(x)^1 o x.n(x)^d(i;p(j))   n(x.n(x)^d(i;p(j))(i)) = j

1 step

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