1. R : Id
2. in : |R|IdLnk
3. out : |R|IdLnk
4. i : |R|
5. j : |R|
6. ring(R;in;out)
  d(i;j)  

By:	Unfold `rdist` 0 THEN GenConcl ((x.n(x)) = n) THEN GenConcl (mu(k.n^k+1(i) = j) = z) THEN Try (DoSubsume THEN Analyze 0 THEN Analyze -1)

1

7. n : |R||R| 8. (x.n(x)) = n   n1:. (k.n^k+1(i) = j)(n1)

6 steps

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