R:(Id), uid:(|R|), out,in:(|R|IdLnk).
  ring(R;in;out)
  
  Inj(|R|; ; uid)
  
  loc.(ring-leader1(loc;R;uid;out;in)) 
  realizes es.ldr:|R|. 
  realizes es.e@ldr.kind(e) = locl("leader")
  realizes es.& (i:|R|. e@i.kind(e) = locl("leader")  i = ldr  |R|)

By:	RealizerSetup 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 THEN Inst Thm* f:(A), L:A List. 0<||L||  (aL.(xL.f(x)f(a))) [|R|;uid;L] THENA Try (Complete Auto) THEN Analyze -1 THEN ExRepD THEN RenameVar `ldr' -3

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. (loc.(ring-leader1(loc;R;uid;out;in)))  Dsys 8. D' : Dsys 9. loc.(ring-leader1(loc;R;uid;out;in))  D' 10. w : World 11. p : FairFifo 12. PossibleWorld(D';w) 13. L : |R| List 14. 0<||L|| 15. i:|R|. (i  L) 16. ldr : |R| 17. (ldr  L) 18. (xL.uid(x)uid(ldr))   ldr:|R|.    e@ldr.kind(e) = locl("leader")   & (i:|R|. e@i.kind(e) = locl("leader")  i = ldr  |R|)

144 steps

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