1. i : Id
2. a : Id
3. T : Type
4. ds : x:Id fp-> Type
5. P : State(ds)TProp
6. init : x:Id fp-> ds(x)?Void
7. x:Id. x  dom(ds)  x  dom(init)
  @i (with ds: ds
  @i init: init
  @i action a:T
  @i precondition a(v) is
  @i P s v) 
  realizes es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id)

By:	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	3. T : Type{i} 4. ds : x:Id fp-> Type{i} 5. P : State(ds)TProp{i} 6. init : x:Id fp-> ds(x)?Void 7. x:Id. x  dom(ds)  x  dom(init)   (es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id))    {es:ES    {| es is an event system of @i (with ds: ds    {| es is an event system of @i init: init    {| 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'}	7 steps
2	@i (with ds: ds   @i init: init   @i action a:T   @i precondition a(v) is   @i P s v) realizes2 es.(v:T. P((x.init(x)?),v))  (e:E. loc(e) = i  Id)	65 steps

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