Def send-once(loc;T;A;a;f;tg;l;x)
Def == [(once(loc;a;source(l))); 
Def == [if loc = source(l)
Def == [if ma-single-sends1(A; Unit; T; x; locl(a); l; tg; (a,b. [(f(a))]))
Def == [else  fi]

is mentioned by

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  (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]

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