1. E : Type
2. EqDecider(E)
3. T : IdIdType
4. V : IdIdType
5. M : IdLnkIdType
6. Top
7. loc : EId
8. kind : EKnd
9. val : e:Eeventtype(kind;loc;V;M;e)
10. when : x:Ide:ET(loc(e),x)
11. after : x:Ide:ET(loc(e),x)
12. sends : l:IdLnkE({m:Msg(M)| haslink(l; m) } List)
13. sender : {e:E| isrcv(kind(e)) }E
14. index : e:{e:E| isrcv(kind(e)) }||sends(lnk(kind(e)),sender(e))||
15. first : E
16. pred : {e':E| first(e') }E
17. causl : EEProp
18. e,e':E. loc(e) = loc(e')  causl(e,e')  e = e'  causl(e',e)
19. e:E. first(e)  (e':E. loc(e') = loc(e)  causl(e',e))
20. e:E. 
20. first(e)
20. 
20. loc(pred(e)) = loc(e) & causl(pred(e),e)
20. & (e':E. loc(e') = loc(e)  (causl(pred(e),e') & causl(e',e)))
21. e:E. first(e)  (x:Id. when(x,e) = after(x,pred(e)))
22. Trans e,e':E. causl(e,e')
23. SWellFounded(causl(e,e'))
24. e:E. 
24. isrcv(kind(e))
24. 
24. (sends(lnk(kind(e)),sender(e)))[(index(e))]
24. =
24. msg(lnk(kind(e));tag(kind(e));val(e))
25. e:E. isrcv(kind(e))  causl(sender(e),e)
26. e,e':E.
26. causl(e,e')
26. 
26. first(e') & causl(e,pred(e'))  e = pred(e')
26.  isrcv(kind(e')) & causl(e,sender(e'))  e = sender(e')
27. e:E. isrcv(kind(e))  loc(e) = destination(lnk(kind(e)))
28. e:E, l:IdLnk. loc(e) = source(l)  sends(l,e) = nil
29. e,e':E.
29. isrcv(kind(e))
29. 
29. isrcv(kind(e'))
29. 
29. lnk(kind(e)) = lnk(kind(e'))
29. 
29. (causl(e,e')
29. (
29. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e'))
30. e:E, l:IdLnk, n:||sends(l,e)||.
30. e':E. isrcv(kind(e')) & lnk(kind(e')) = l & sender(e') = e & index(e') = n
31. Top
  e:E. 
  first(e)
  
  loc(pred(e)) = loc(e) & causl(pred(e),e)
  & (e':E. 
  & ((loc(pred(e)) = loc(e') & causl(pred(e),e')
  & ((& loc(e') = loc(e)
  & ((& causl(e',e)))

By:	AllHyps (i. (((ParallelOp i THEN RepeatFor 3 (ParallelOp -1) THEN Analyze 0) ((THEN (((Analyze -2) ((THEN (((Analyze -1)) (THEN (Complete Auto)

None

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