i:Id, L:Knd List, x:Id, T:Type.
  @i: only L affects x : T 
  realizes es.(vartype(i;x) r T)
  realizes es.& (e:E. 
  realizes es.& (loc(e) = i  Id
  realizes es.& (
  realizes es.& (((x after e) = (x when e)  T  (kind(e)  L))
  realizes es.& (& ((kind(e)  L)  (x after e) = (x when e)  T))

By:	Auto THEN Try (ParallelOp 1) THEN BackThru Thm* D:Dsys, P:({es:ES| es is an event system of D }Prop{i'}). Thm* D realizes2 es.P(es)  D realizes es.P(es) THENA Try (Complete Auto)

1	1. i : Id 2. L : Knd List 3. x : Id 4. T : Type{i}   (es.(vartype(i;x) r T)   (& (e:E.    (& (loc(e) = i  Id   (& (   (& (((x after e) = (x when e)  T  (kind(e)  L))   (& (& ((kind(e)  L)  (x after e) = (x when e)  T)))    {es:ES| es is an event system of @i: only L affects x : T }Prop{i'}	1 step
2	1. i : Id 2. L : Knd List 3. x : Id 4. T : Type   @i: only L affects x : T realizes2 es.(vartype(i;x) r T)   & (e:E.    & (loc(e) = i  Id   & (   & (((x after e) = (x when e)  T  (kind(e)  L))   & (& ((kind(e)  L)  (x after e) = (x when e)  T))	15 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html