1. i : Id
2. T : Type
3. v : T
4. x : Id
  (es.(vartype(i;x) r T)
  (& (e:E. loc(e) = i  Id  first(e)  (x when e) = v  T))
   {es:ES| es is an event system of @i: x:T initially x = v }Prop{i'}

1

2. T : Type 3. v : T 4. x : Id 5. es : ES 6. w : World 7. p : FairFifo 8. PossibleWorld(@i: x:T 8. PossibleWorld(@i: xinitially x = v;w) 9. es = ES(w)  ES 10. vartype(i;x) r T 11. e : E 12. loc(e) = i  Id 13. first(e)   (x when e)  T

3 steps

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