R:(Id), uid:(|R|), out,in:(|R|IdLnk).
  ring(R;in;out)
  
  Inj(|R|; ; uid)  d-feasible(loc.(ring-leader1(loc;R;uid;out;in)))

By:	Auto THEN Inst Thm* R:(Id), in,out:(|R|IdLnk). Thm* ring(R;in;out)  (L:|R| List. 0<||L|| & (i:|R|. (i  L))) [R;in;out] THEN ExRepD

1

1. R : Id 2. uid : |R| 3. out : |R|IdLnk 4. in : |R|IdLnk 5. ring(R;in;out) 6. Inj(|R|; ; uid) 7. L : |R| List 8. 0<||L|| 9. i:|R|. (i  L)   d-feasible(loc.(ring-leader1(loc;R;uid;out;in)))

12 steps

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