i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp).
  @i (with ds: ds
  @i action a:T
  @i precondition a(v) is
  @i P s v) 
  realizes es.(x:Id. vartype(i;x) r ds(x)?Top)
  realizes es.& (e:E. 
  realizes es.& (loc(e) = i  Id
  realizes es.& (
  realizes es.& (kind(e) = locl(a)  Knd  (valtype(e) r T))
  realizes es.& (e:E. 
  realizes es.& (loc(e) = i  Id
  realizes es.& (
  realizes es.& ((kind(e) = locl(a)  Knd  P((z.(z when e)),val(e)))
  realizes es.& (& (e':E. 
  realizes es.& (& ((e <loc e')  e = e'  E
  realizes es.& (& (& kind(e') = locl(a)  Knd
  realizes es.& (& (&  (v:T. P((z.(z after e')),v))))

By:	Auto 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. a : Id 3. T : Type{i} 4. ds : x:Id fp-> Type{i} 5. P : State(ds)TProp{i}   (es.(x:Id. vartype(i;x) r ds(x)?Top)   (& (e:E. loc(e) = i  Id  kind(e) = locl(a)  Knd  (valtype(e) r T))   (& (e:E.    (& (loc(e) = i  Id   (& (   (& ((kind(e) = locl(a)  Knd  P((z.(z when e)),val(e)))   (& (& (e':E.    (& (& ((e <loc e')  e = e'  E   (& (& (& kind(e') = locl(a)  Knd  (v:T. P((z.(z after e')),v)))))    {es:ES    {| es is an event system of @i (with ds: ds    {| es is an event system of @i action a:T    {| es is an event system of @i precondition a(v) is    {| es is an event system of @i P s v) }    Prop{i'}	1 step
2	1. i : Id 2. a : Id 3. T : Type 4. ds : x:Id fp-> Type 5. P : State(ds)TProp   @i (with ds: ds   @i action a:T   @i precondition a(v) is   @i P s v) realizes2 es.(x:Id. vartype(i;x) r ds(x)?Top)   & (e:E. loc(e) = i  Id  kind(e) = locl(a)  Knd  (valtype(e) r T))   & (e:E.    & (loc(e) = i  Id   & (   & ((kind(e) = locl(a)  Knd  P((z.(z when e)),val(e)))   & (& (e':E.    & (& ((e <loc e')  e = e'  E   & (& (& kind(e') = locl(a)  Knd  (v:T. P((z.(z after e')),v))))	162 steps

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