is mentioned by

Thm* x:Id, L:Top, t:Type, x1:Id, L1:Top, t1:Type. Thm* x = x1 Thm*  Thm* only members of L affect x :t ||+ only members of L1 affect x1 :t1	[ma-single-frame-ma-single-frame-compatible]
Thm* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top. Thm* x : t || x1 : t1 Thm*  Thm* x1 : t1 initially x1 = v ||+ only members of L affect x :t	[ma-single-init-ma-single-frame-compatible]
Thm* x:Id, L:Top, t:Type, x1:Id, t1:Type, v:Top. Thm* x : t || x1 : t1 Thm*  Thm* only members of L affect x :t ||+ x1 : t1 initially x1 = v	[ma-single-frame-ma-single-init-compatible]
Thm* l:IdLnk, tg:Id, L:Top, x:Id, L1,t:Top. Thm* only members of L1 affect x :t ||+ only L sends on (l with tg)	[ma-single-frame-ma-single-sframe-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, Thm* L:Knd List, t:Type. Thm* ds || x1 : t Thm*  Thm* (x = x1  (k  L)) Thm*  Thm* only members of L affect x1 :t ||+ ma-single-effect(ds; da; k; x; f)	[ma-single-frame-ma-single-effect-compatible]
Thm* x:Id, k:Knd, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:Top, x1:Id, Thm* L:Knd List, t:Type. Thm* ds || x1 : t Thm*  Thm* (x = x1  (k  L)) Thm*  Thm* ma-single-effect(ds; da; k; x; f) ||+ only members of L affect x1 :t	[ma-single-effect-ma-single-frame-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, L:Top, t:Type. Thm* ds || x : t Thm*  Thm* only members of L affect x :t ||+ ma-single-sends(ds; da; k; l; f)	[ma-single-frame-ma-single-sends-compatible]
Thm* k:Knd, l:IdLnk, ds:x:Id fp-> Type, da:a:Knd fp-> Top, f:(IdTop) List, Thm* x:Id, L:Top, t:Type. Thm* ds || x : t Thm*  Thm* ma-single-sends(ds; da; k; l; f) ||+ only members of L affect x :t	[ma-single-sends-ma-single-frame-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type. Thm* ds || x : t Thm*  Thm* only members of L affect x :t ||+ (with ds: ds Thm* oaction a:T Thm* oprecondition a(v) is Thm* oP s v)	[ma-single-frame-ma-single-pre-compatible]
Thm* a:Id, T:Type, ds:x:Id fp-> Type, P:Top, x:Id, L:Top, t:Type. Thm* ds || x : t Thm*  Thm* (with ds: ds Thm* (action a:T Thm* (precondition a(v) is Thm* (P s v) ||+ only members of L affect x :t	[ma-single-pre-ma-single-frame-compatible]
Thm* a:Id, T:Top, ds:x:Id fp-> Type, P:Top, init:x:Id fp-> Top, x:Id, Thm* L:Knd List, t:Type. Thm* ds || x : t Thm*  Thm* (with ds: ds Thm* (init: init Thm* action a:T Thm* aprecondition a(v) is Thm* aP) ||+ only members of L affect x :t	[ma-single-pre-init-ma-single-frame-compatible]
Thm* i,x:Id, k:Knd, T:Type. Thm* @i: only members of [k] affect x :T  Dsys Thm* & (D:Dsys.  Thm* & (@i: only members of [k] affect x :T  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(i;x) r T) Thm* & (realizes es.& e@i.((x after e) = (x when e)  T  kind(e) = k  Knd) Thm* & (realizes es.& & (kind(e) = k  Knd  (x after e) = (x when e)  T))	[frame-rule1]
Thm* i,x:Id, T:Type. Thm* @i: only members of nil affect x :T  Dsys Thm* & (D:Dsys.  Thm* & (@i: only members of nil affect x :T  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(i;x) r T) & e@i.(x after e) = (x when e)  T)	[frame-rule0]
Thm* i:Id, L:Knd List, x:Id, T:Type. Thm* @i: only members of L affect x :T  Dsys Thm* & (D:Dsys.  Thm* & (@i: only members of L affect x :T  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(i;x) r T) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (((x after e) = (x when e)  T  (kind(e)  L)) Thm* & (realizes es.& (& ((kind(e)  L)  (x after e) = (x when e)  T)))	[s-frame-rule]
Def recognizer1(loc;T;A;P;k;i;r;x) Def == if loc = i Def == if [r :  initially r = false;  Def == if [only members of [k] affect r :;  Def == if [ma-single-effect1(r;;x;A;k;T;r,x,v. P(x,v)  r)] Def == else nil fi	[recognizer1]
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]
Def Dconstant(loc;T;c;x;i) Def == if loc = i [x : T initially x = c; only members of nil affect x :T] Def == else nil fi	[Dconstant]

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

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