is mentioned by

Thm* P:(AT), k:Knd, i,r,x:Id. Thm* A Thm*  Thm* T Thm*  Thm* x = r Thm*  Thm* loc.(recognizer1(loc;T;A;P;k;i;r;x))  Thm* realizes es.e@i.kind(e) = k  Knd  (valtype(e) r T) Thm* realizes es.& (vartype(i;x) r A) Thm* realizes es.& e@i.first(e)  (r when e) = false   Thm* realizes es.& e'@i.(r after e') Thm* realizes es.& e'@i. Thm* realizes es.& e'@i.(e:E.  Thm* realizes es.& e'@i.((e <loc e')  e = e'  E Thm* realizes es.& e'@i.(& kind(e) = k  Knd Thm* realizes es.& e'@i.(& P((x when e),val(e)))	[recognizer1__realizes]
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,a,x:Id, A,T:Type, c:A, P:(ATProp). Thm* @i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v))  Dsys Thm* & (D:Dsys.  Thm* & (@i: ma-single-pre-init1(x;A;c;a;T;x,v.P(x,v))  D Thm* & ( Thm* & (D  Thm* & (realizes es.(vartype(i;x) r A) Thm* & (realizes es.& (e:E. loc(e) = i  Id  first(e)  (x when e) = c  A) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T)) Thm* & (realizes es.& (e:E.  Thm* & (realizes es.& (loc(e) = i  Id Thm* & (realizes es.& ( Thm* & (realizes es.& (kind(e) = locl(a)  Knd  P((x when e),val(e))) Thm* & (realizes es.& & ((v:T. P(c,v)) Thm* & (realizes es.& & ( Thm* & (realizes es.& & ((e:E.  Thm* & (realizes es.& & ((loc(e) = i  Id Thm* & (realizes es.& & ((& kind(e) = locl(a)  Knd Thm* & (realizes es.& & ((&  (v:T. P((x after e),v)))))	[s-pre-init-rule1]
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]

In prior sections: mb event system 2 mb event system 3 mb event system 6

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