i,a:Id, T:Type, ds:x:Id fp-> Type, P:(State(ds)TProp),
  init:x:Id fp-> ds(x)?Void.
  (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)

1

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)

73 steps

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