R:(Id), in,out:(|R|IdLnk).
  ring(R;in;out)  (i,j:|R|. n(i) = n(j)  i = j)

1

1. R : Id 2. in : |R|IdLnk 3. out : |R|IdLnk 4. i:|R|.  4. R(source(in(i))) & R(destination(out(i))) 4. & source(out(i)) = i 4. & & destination(in(i)) = i 4. & & in(destination(out(i))) = out(i) 4. & & out(source(in(i))) = in(i) 5. i,j:|R|. k:. x.destination(out(x))^k(i) = j  Id 6. |R| 7. i : |R| 8. j : |R| 9. destination(out(i)) = destination(out(j))  |R| 10. R(source(in(i))) 11. R(destination(out(i))) 12. source(out(i)) = i 13. destination(in(i)) = i 14. in(destination(out(i))) = out(i) 15. out(source(in(i))) = in(i) 16. R(source(in(j))) 17. R(destination(out(j))) 18. source(out(j)) = j 19. destination(in(j)) = j 20. in(destination(out(j))) = out(j) 21. out(source(in(j))) = in(j) 22. in(destination(out(i))) = in(destination(out(j))) 23. out(i) = out(j) 24. source(out(i)) = source(out(j)) 25. i = j  Id   i = j

1 step

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