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':E.
  isrcv(kind(e))
  
  isrcv(kind(e'))
  
  lnk(kind(e)) = lnk(kind(e'))
  
  (loc(e) = loc(e') & causl(e,e')
  (
  (loc(sender(e)) = loc(sender(e')) & causl(sender(e),sender(e'))
  ( sender(e) = sender(e') & index(e)<index(e'))

1	32. e : E 33. e':E.  33. isrcv(kind(e)) 33.  33. isrcv(kind(e')) 33.  33. lnk(kind(e)) = lnk(kind(e')) 33.  33. (causl(e,e') 33. ( 33. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e')) 34. e' : E 35. isrcv(kind(e)) 36. isrcv(kind(e')) 37. lnk(kind(e)) = lnk(kind(e')) 38. causl(e,e') 38.  38. causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e') 39. (causl(e,e'))  (causl(sender(e),sender(e')) 39.  sender(e) = sender(e') & index(e)<index(e')) 40. loc(e) = loc(e') 41. causl(e,e')   loc(sender(e)) = loc(sender(e')) & causl(sender(e),sender(e'))    sender(e) = sender(e') & index(e)<index(e')	8 steps
2	32. e : E 33. e':E.  33. isrcv(kind(e)) 33.  33. isrcv(kind(e')) 33.  33. lnk(kind(e)) = lnk(kind(e')) 33.  33. (causl(e,e') 33. ( 33. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e')) 34. e' : E 35. isrcv(kind(e)) 36. isrcv(kind(e')) 37. lnk(kind(e)) = lnk(kind(e')) 38. causl(e,e') 38.  38. causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e') 39. (causl(e,e'))  (causl(sender(e),sender(e')) 39.  sender(e) = sender(e') & index(e)<index(e')) 40. loc(sender(e)) = loc(sender(e')) & causl(sender(e),sender(e')) 40.  sender(e) = sender(e') & index(e)<index(e')   loc(e) = loc(e')	1 step
3	32. e : E 33. e':E.  33. isrcv(kind(e)) 33.  33. isrcv(kind(e')) 33.  33. lnk(kind(e)) = lnk(kind(e')) 33.  33. (causl(e,e') 33. ( 33. (causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e')) 34. e' : E 35. isrcv(kind(e)) 36. isrcv(kind(e')) 37. lnk(kind(e)) = lnk(kind(e')) 38. causl(e,e') 38.  38. causl(sender(e),sender(e'))  sender(e) = sender(e') & index(e)<index(e') 39. (causl(e,e'))  (causl(sender(e),sender(e')) 39.  sender(e) = sender(e') & index(e)<index(e')) 40. loc(sender(e)) = loc(sender(e')) & causl(sender(e),sender(e')) 40.  sender(e) = sender(e') & index(e)<index(e')   causl(e,e')	1 step

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