Def ring-leader1(loc;R;uid;out;in)
Def == if R(loc)
Def == if [(send-once(loc;;;"send-me";x.x;"vote";out(loc);"me")); 
Def == if [(trigger1(loc;;;x,y. x=y;loc;rcv
Def == if [((in(loc)); "vote");"leader";"me")); 
Def == if [(Dconstant(loc;;uid(loc);"me";loc)); 
Def == if [ma-single-sends1(;
Def == if [ma-single-sends1(;
Def == if [ma-single-sends1(;
Def == if [ma-single-sends1("me";
Def == if [ma-single-sends1(rcv((in(loc)); "vote");
Def == if [ma-single-sends1((out(loc));
Def == if [ma-single-sends1("vote";
Def == if [ma-single-sends1((a,b. if a<b [b] else nil fi)); 
Def == if [only [rcv((in(loc)); "vote"); 
Def == if [only [locl("send-me")] sends on (out(loc) with "vote")]
Def == else nil fi

is mentioned by

Thm* R:(Id), uid:(|R|), out,in:(|R|IdLnk). Thm* ring(R;in;out) Thm*  Thm* Inj(|R|; ; uid) Thm*  Thm* loc.(ring-leader1(loc;R;uid;out;in))  Thm* realizes es.ldr:|R|.  Thm* realizes es.e@ldr.kind(e) = locl("leader") Thm* realizes es.& (i:|R|. e@i.kind(e) = locl("leader")  i = ldr  |R|)	[ring-leader1__realizes]
Thm* R:(Id), uid:(|R|), out,in:(|R|IdLnk). Thm* ring(R;in;out) Thm*  Thm* Inj(|R|; ; uid)  d-feasible(loc.(ring-leader1(loc;R;uid;out;in)))	[ring-leader1__feasible]
Thm* loc:Id, R:(Id), uid:(|R|), out,in:(|R|IdLnk). Thm* ring(R;in;out) Thm*  Thm* Inj(|R|; ; uid)  (A,Bring-leader1(loc;R;uid;out;in).A ||+ B)	[ring-leader1__compatible]

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html