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
11. x  dom(init)
    ds(x)?Top

1

12. x  dom(ds)     ds(x)

1 step

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