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* P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm*  Thm* T Thm*  Thm* x = "trigger" Thm*  Thm* locl(a) = k Thm*  Thm* loc.(trigger1(loc;T;A;P;i;k;a;x))  Thm* realizes es.(vartype(i;x) r A) Thm* realizes es.& e@i.kind(e) = k  Knd  (valtype(e) r T) Thm* realizes es.& e'@i.kind(e') = locl(a) Thm* realizes es.& e'@i. Thm* realizes es.& (e:E.  Thm* realizes es.& ((e <loc e') & kind(e) = k  Knd & P((x when e),val(e))) Thm* realizes es.& e@i.kind(e) = k  Knd Thm* realizes es.& e@i. Thm* realizes es.& P((x when e),val(e))  e'@i.kind(e') = locl(a)  Knd	[trigger1__realizes]
Thm* P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm*  Thm* T Thm*  Thm* x = "trigger" Thm*  Thm* locl(a) = k  d-feasible(loc.(trigger1(loc;T;A;P;i;k;a;x)))	[trigger1__feasible]
Thm* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm*  Thm* T Thm*  Thm* x = "trigger"  locl(a) = k  trigger1(loc;T;A;P;i;k;a;x)  MsgA List	[trigger1_wf]
Thm* loc:Id, T,A:Type, P:(AT), i:Id, k:Knd, a,x:Id. Thm* A Thm*  Thm* T Thm*  Thm* x = "trigger" Thm*  Thm* locl(a) = k  (A,Btrigger1(loc;T;A;P;i;k;a;x).A ||+ B)	[trigger1__compatible]
Thm* a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. Thm* "done" = x Thm*  Thm* A Thm*  Thm* T Thm*  Thm* loc.(send-once(loc;T;A;a;f;tg;l;x))  Thm* realizes es.(vartype(source(l);x) r A) Thm* realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T)) Thm* realizes es.& (e:E.  Thm* realizes es.& (kind(e) = rcv(l; tg)  Knd Thm* realizes es.& (& val(e) = f((x when sender(e)))  T Thm* realizes es.& (& & kind(sender(e)) = locl(a)  Knd Thm* realizes es.& (& & (e':E.  Thm* realizes es.& (& & (kind(e') = rcv(l; tg)  Knd Thm* realizes es.& (& & ( Thm* realizes es.& (& & (kind(sender(e')) = locl(a)  Knd  e' = e  E))	[send-once__realizes]
Thm* a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. Thm* "done" = x  A  T  d-feasible(loc.(send-once(loc;T;A;a;f;tg;l;x)))	[send-once__feasible]
Thm* loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. Thm* "done" = x  A  T  send-once(loc;T;A;a;f;tg;l;x)  MsgA List	[send-once_wf]
Thm* loc:Id, T,A:Type, a:Id, f:(AT), tg:Id, l:IdLnk, x:Id. Thm* "done" = x  A  T  (A,Bsend-once(loc;T;A;a;f;tg;l;x).A ||+ B)	[send-once__compatible]
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	[ring-leader1]
Def trigger1(loc;T;A;P;i;k;a;x) Def == [(recognizer1(loc;T;A;P;k;i;"trigger";x));  Def == [if loc = i ma-single-pre1("trigger";;a;Unit;x,v.x) else  fi]	[trigger1]
Def once(loc;a;i) Def == if loc = i Def == if [ma-single-pre-init1("done";;false;a;Unit;x,v.x);  Def == if [only members of [locl(a)] affect "done" :;  Def == if [ma-single-effect0("done";;locl(a);Unit;x,v. true)] Def == else nil fi	[once]

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