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* L:Knd List, l:IdLnk, tg:Id. Thm* @source(l): only L sends on (l with tg)  Dsys Thm* & (D:Dsys.  Thm* & (@source(l): only L sends on (l with tg)  D Thm* & ( Thm* & (D  Thm* & (realizes es.e:E.  Thm* & (realizes es.loc(e) = destination(l)  Id Thm* & (realizes es. Thm* & (realizes es.kind(e) = rcv(l; tg)  Knd  (kind(sender(e))  L))	[better-sframe-rule]
Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type. Thm* (rcv(l; tg) = k  T = B) Thm*  Thm* (f:(ABT), c:(AB). Thm* (@source(l): ma-single-sends1(A; Thm* (@source(l): ma-single-sends1(B; Thm* (@source(l): ma-single-sends1(T; Thm* (@source(l): ma-single-sends1(x; Thm* (@source(l): ma-single-sends1(k; Thm* (@source(l): ma-single-sends1(l; Thm* (@source(l): ma-single-sends1(tg; Thm* (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi)) Thm* ( Dsys Thm* (& (D:Dsys.  Thm* (& (@source(l): ma-single-sends1(A; Thm* (& (@source(l): ma-single-sends1(B; Thm* (& (@source(l): ma-single-sends1(T; Thm* (& (@source(l): ma-single-sends1(x; Thm* (& (@source(l): ma-single-sends1(k; Thm* (& (@source(l): ma-single-sends1(l; Thm* (& (@source(l): ma-single-sends1(tg; Thm* (& (@source(l): ma-single-sends1((a,b. if c(a,b) [(f(a,b))] else nil fi) Thm* (& (@source(l): ma-single-sends1()  D Thm* (& ( Thm* (& (D  Thm* (& (realizes es.(vartype(source(l);x) r A) Thm* (& (realizes es.& (e:E.  Thm* (& (realizes es.& (loc(e) = source(l)  Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k  Knd  (valtype(e) r B)) Thm* (& (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T)) Thm* (& (realizes es.& (e:E.  Thm* (& (realizes es.& (loc(e) = source(l)  Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k  Knd Thm* (& (realizes es.& ( Thm* (& (realizes es.& ((c((x when e),val(e)) Thm* (& (realizes es.& (( Thm* (& (realizes es.& (((e':E.  Thm* (& (realizes es.& (((kind(e') = rcv(l; tg)  Knd Thm* (& (realizes es.& (((& sender(e') = e  E Thm* (& (realizes es.& (((& & (e'':E.  Thm* (& (realizes es.& (((& & (kind(e'') = rcv(l; tg)  Knd Thm* (& (realizes es.& (((& & ( Thm* (& (realizes es.& (((& & (sender(e'') = e  E  e'' = e'  E) Thm* (& (realizes es.& (((& & val(e') = f((x when e),val(e))  T)) Thm* (& (realizes es.& (& (c((x when e),val(e)) Thm* (& (realizes es.& (& ( Thm* (& (realizes es.& (& ((e':E.  Thm* (& (realizes es.& (& ((kind(e') = rcv(l; tg)  Knd Thm* (& (realizes es.& (& ((& sender(e') = e  E)))))	[conditional-send1-rule]
Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type. Thm* (rcv(l; tg) = k  T = B) Thm*  Thm* (f:(ABT).  Thm* (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))])) Thm* ( Dsys Thm* (& (D:Dsys.  Thm* (& (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; (a,b. [(f(a,b))]) Thm* (& (@source(l): ma-single-sends1()  D Thm* (& ( Thm* (& (D  Thm* (& (realizes es.(vartype(source(l);x) r A) Thm* (& (realizes es.& (e:E.  Thm* (& (realizes es.& (loc(e) = source(l)  Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k  Knd  (valtype(e) r B)) Thm* (& (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T)) Thm* (& (realizes es.& (e:E.  Thm* (& (realizes es.& (loc(e) = source(l)  Id Thm* (& (realizes es.& ( Thm* (& (realizes es.& (kind(e) = k  Knd Thm* (& (realizes es.& ( Thm* (& (realizes es.& ((e':E.  Thm* (& (realizes es.& ((kind(e') = rcv(l; tg)  Knd Thm* (& (realizes es.& ((& sender(e') = e  E Thm* (& (realizes es.& ((& & (e'':E.  Thm* (& (realizes es.& ((& & (kind(e'') = rcv(l; tg)  Knd Thm* (& (realizes es.& ((& & ( Thm* (& (realizes es.& ((& & (sender(e'') = e  E  e'' = e'  E) Thm* (& (realizes es.& ((& & val(e') = f((x when e),val(e))  T))))	[s-unconditional-send1-rule]
Thm* x,tg:Id, k:Knd, l:IdLnk, T,A,B:Type, f:(AB(T List)). Thm* (rcv(l; tg) = k  T = B) Thm*  Thm* @source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  Dsys Thm* & (D:Dsys.  Thm* & (@source(l): ma-single-sends1(A; B; T; x; k; l; tg; f)  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(source(l);x) r A) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = source(l)  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = k  Knd  (valtype(e) r B)) Thm* & (realizes es.& (e:E. kind(e) = rcv(l; tg)  Knd  (valtype(e) r T)) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = source(l)  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = k  Knd Thm* & (realizes es.& ( Thm* & (realizes es.& ((L:{e':E| kind(e') = rcv(l; tg)  Knd } List.  Thm* & (realizes es.& (((e':E.  Thm* & (realizes es.& ((((e'  L) Thm* & (realizes es.& ((( Thm* & (realizes es.& (((kind(e') = rcv(l; tg)  Knd & sender(e') = e  E) Thm* & (realizes es.& ((& (e1,e2:E. e1 before e2  L  (e1 <loc e2)) Thm* & (realizes es.& ((& map(e'.val(e');L) = f((x when e),val(e))  T List)))	[s-sends-rule1]
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]

In prior sections: mb event system 1 mb event system 2 mb event system 3 mb event system 5 mb event system 6 mb event system 4

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