2. Trans e,e':E. (e <loc e')
3. SWellFounded((e <loc e'))
4.
e,e':E. loc(e) = loc(e') 
(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. first(e) (x:Id. (x when e) = (x after pred(e)))
8. Trans e,e':E. (e < e')
9. SWellFounded((e < e'))
10.
e:E.
10. isrcv(e)
sends(lnk(e);sender(e))[index(e)] = msg(lnk(e);tag(e);val(e))
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')
13.
isrcv(e') & (e < sender(e')) e = sender(e')
14.
e:E. isrcv(e) loc(e) = destination(lnk(e))
15.
e:E, l:IdLnk. loc(e) = source(l) sends(l;e) = nil
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'))
sender(e) = sender(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 & index(e') = n
18. e : E
19. e' : E
20. (e <loc e')
first(e')
