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. 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. Id
  loc(e) = loc(pred(e))

None

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