the_es:ES, e,e':E.
(e <loc e') 
first(e') & e = pred(e') 
E 
(e <loc pred(e')) the_es:ES, e,e':E.
(e <loc e') first(e') & e = pred(e') E (e <loc pred(e'))| By: |
|
| 1 |
2. Trans e,e':E. (e <loc e') 3. SWellFounded((e <loc e')) 4. e,e':E. loc(e) = loc(e') Id (e <loc e') e = e' (e' <loc e)
5. e:E. first(e) (e':E. (e' <loc e))
6. e:E.
6. first(e)  (pred(e) <loc e) & (e':E. ((pred(e) <loc e') & (e' <loc e)))
7. e:E.
7. first(e) (x:Id. (x when e) = (x after pred(e)) vartype(loc(e);x))
8. Trans e,e':E. (e < e') 9. SWellFounded((e < e')) 10. e:E.
10. isrcv(e) 10.
10. sends(lnk(e);sender(e))[index(e)] = msg(lnk(e);tag(e);val(e)) Msg
11. e,e':E. (e <loc e') (e < e')
12. e:E. isrcv(e) (sender(e) < e)
13. e,e':E.
13. (e < e') 13.
13. first(e') & (e < pred(e')) e = pred(e') E
13. isrcv(e') & (e < sender(e')) e = sender(e') E
14. e:E. isrcv(e) loc(e) = destination(lnk(e))
15. e:E, l:IdLnk. loc(e) = source(l) sends(l;e) = nil (Msg on l) List
16. e,e':E.
16. isrcv(e) 16.
16. isrcv(e') 16.
16. lnk(e) = lnk(e') 16.
16. ((e <loc e') 16. (
16. ((sender(e) <loc sender(e')) 16. ( sender(e) = sender(e') E & index(e)<index(e'))
17. e:E, l:IdLnk, n: ||sends(l;e)||.
17.  e':E. isrcv(e') & lnk(e') = l & sender(e') = e E & index(e') = n 
e,e':E. (e <loc e') first(e') & e = pred(e') E (e <loc pred(e')) | 15 steps |
About:
 |  |  |  |  |