1. i : Id
2. x : Id
3. k : Knd
4. ds : x:Id fp-> Type
5. da : a:Knd fp-> Type
6. f : State(ds)ma-valtype(da; k)ds(x)?Void
  d-single-effect(i; ds; da; k; x; f) realizes2 es.(x:Id. 
  d-single-effect(i; ds; da; k; x; f) realizes2 es.(vartype(i;x) r ds(x)?Top)
  & (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))
  & (e:E. 
  & (loc(e) = i  Id
  & (
  & (kind(e) = k  Knd  (x after e) = f((z.(z when e)),val(e))  ds(x)?Top)

1	7. w : World 8. p : FairFifo 9. PossibleWorld(d-single-effect(i; ds; da; k; x; f);w)   (x:Id. vartype(i;x) r ds(x)?Top)   & (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))	16 steps
2	7. w : World 8. p : FairFifo 9. PossibleWorld(d-single-effect(i; ds; da; k; x; f);w) 10. (x:Id. vartype(i;x) r ds(x)?Top) 10. & (e:E. loc(e) = i  Id  (valtype(e) r ma-valtype(da; kind(e))))   e:E.    loc(e) = i  Id      kind(e) = k  Knd  (x after e) = f((z.(z when e)),val(e))  ds(x)?Top	23 steps

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