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|)

By:	InstConcl [ldr] THENA (Auto THEN AllHyps (h.Analyze h THEN Complete Auto))

1

e@ldr.kind(e) = locl("leader")   & (i:|R|. e@i.kind(e) = locl("leader")  i = ldr  |R|)

143 steps

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