mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def ma-single-sends1(A; B; T; x; a; l; tg; f)
Def == ma-single-sends(x : A;
Def == ma-single-sends(a : B  rcv(l; tg) : T;
Def == ma-single-sends(a;
Def == ma-single-sends(l;
Def == ma-single-sends([<tg,s,v. f(s(x),v)>])

is mentioned by

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]
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]		[send-once]

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

mb event system 7 Sections EventSystems Doc