1. the_w : World
2. l : IdLnk
3. e : E
4. v : {m:Msg(the_w.M)| source(mlnk(m)) = loc(e) } List
5. m(loc(e);time(e)) = v
6. v  Msg(the_w.M) List
  ({m:Msg(the_w.M)| (ms.mlnk(ms) = l)(m) } List) r ({m:Msg(the_w.M)
  ({m:Msg(the_w.M)| (ms.mlnk(ms) = l)(m) } List) r ({| mlnk(m) = l } List)

1

7. x : Msg(the_w.M) 8. mlnk(x) = l   mlnk(x) = l

1 step

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