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)
8. {es:ES
8. {| es is an event system of @i (with ds: ds
8. {| es is an event system of @i init: init
8. {| es is an event system of @i action a:T
8. {| es is an event system of @i precondition a(v) is
8. {| es is an event system of @i P s v) }
9. T
10. x : Id
  init(x)?  ds(x)?Top

1	11. x  dom(init)   init(x)  ds(x)?Top	1 step
2	11. x  dom(init)     ds(x)?Top	2 steps

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