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)
  (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'}

1

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)

6 steps

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