Def MsgA
Def == ds:x:Id fp-> Type
Def == da:a:Knd fp-> Type
Def == x:Id fp-> ds(x)?Voida:Id fp-> State(ds)ma-valtype(da; locl(a))Prop
Def == kx:KndId fp-> State(ds)ma-valtype(da; 1of(kx))ds(2of(kx))?Void
Def == kl:KndIdLnk fp-> (tg:Id
Def == kl:KndIdLnk fp-> (State(ds)ma-valtype(da; 1of(kl))
Def == kl:KndIdLnk fp-> ((da(rcv(2of(kl); tg))?Void List)) List
Def == x:Id fp-> Knd Listltg:IdLnkId fp-> Knd ListTop

is mentioned by

Thm* loc:Id, R:(Id), uid:(|R|), out,in:(|R|IdLnk). Thm* ring(R;in;out) Thm*  Thm* Inj(|R|; ; uid)  ring-leader1(loc;R;uid;out;in)  MsgA List	[ring-leader1_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"  locl(a) = k  trigger1(loc;T;A;P;i;k;a;x)  MsgA List	[trigger1_wf]
Thm* loc:Id, T,A:Type, P:(AT), k:Knd, i,r,x:Id. Thm* A  T  x = r  recognizer1(loc;T;A;P;k;i;r;x)  MsgA List	[recognizer1_wf]
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,a,i:Id. once(loc;a;i)  MsgA List	[once_wf]
Thm* loc:Id, T:Type, c:T, x,i:Id. Dconstant(loc;T;c;x;i)  MsgA List	[Dconstant_wf]

In prior sections: mb event system 5 mb event system 6

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