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
  (x.init(x)?)  State(ds)

1	10. x : Id   init(x)?  ds(x)?Top	4 steps
2	Id  Type	Auto

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