1. E : Type
2. T : IdIdType
3. V : IdIdType
4. M : IdLnkIdType
5. loc : EId
6. kind : EKnd
7. e:Eeventtype(kind;loc;V;M;e)
8. x:Ide:ET(loc(e),x)
9. after : x:Ide:ET(loc(e),x)
10. sends : l:IdLnkE(Msg_sub(l; M) List)
11. sender : {e:E| isrcv(kind(e)) }E
12. e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
13. first : E
14. pred : {e':E| first(e') }E
15. causl : EEProp
16. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
17. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
18. e:E. 
18. first(e)
18. 
18. loc(pred(e)) = loc(e) & causl(pred(e),e)
18. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
19. e : E
20. first(e)
21. x : Id
  after(x,pred(e))  T(loc(e),x)

1	loc(e) = loc(pred(e))	1 step
2	22. loc(e) = loc(pred(e))   T(loc(pred(e)),x) = T(loc(e),x)	1 step

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