2.
i:Id, t:
, l:IdLnk. 
source(l) = i 
onlnk(l;m(i;t)) = nil
3. (
i:Id, t:. isnull(a(i;t)) (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil)
3. & (
i:Id, t:, l:IdLnk.
3. & (isrcv(l;a(i;t))
3. & (
3. & (destination(l) = i & ||queue(l;t)||
1 & hd(queue(l;t)) = msg(a(i;t)))
3. & (
l:IdLnk, t:.
3. & (
t':. t
t' & isrcv(l;a(destination(l);t')) 
queue(l;t') = nil)
4.
e,e':E. loc(e) = loc(e') e <c e' e = e' e' <c e
5.
e:E. first(e) 
(e':E. loc(e') = loc(e) e' <c e)
6.
e:E.
6.
first(e)
6.
6. loc(pred(e)) = loc(e) & pred(e) <c e
6. & (
e':E. loc(e') = loc(e) (pred(e) <c e' & e' <c e))
7.
e:E. first(e) (x:Id. (x when e) = (x after pred(e)))
8. Trans e,e':E. e <c e'
9. SWellFounded(e <c e')
10.
e:E.
10. isrcv(kind(e))
10.
10. sends(lnk(kind(e));sender(e))[index(e)]
10. =
10. msg(lnk(kind(e));tag(kind(e));val(e))
11.
e:E. isrcv(kind(e)) sender(e) <c e
12.
e,e':E.
12. e <c e'
12.
12.
first(e') & e <c pred(e') e = pred(e')
12.
isrcv(kind(e')) & e <c sender(e') e = sender(e')
13.
e:E. isrcv(kind(e)) loc(e) = destination(lnk(kind(e)))
14.
e:E, l:IdLnk. loc(e) = source(l) sends(l;e) = nil
15.
e,e':E.
15. isrcv(kind(e))
15.
15. isrcv(kind(e'))
15.
15. lnk(kind(e)) = lnk(kind(e'))
15.
15. (e <c e'
15. (
15. (sender(e) <c sender(e')
sender(e) = sender(e') & index(e)<index(e'))
16.
m:, l:IdLnk, t:. m||snds(l;t)|| (t':. tt' & m||rcvs(l;t')||)
17. e1 : Id
18. e2 :
19.
isnull(a(e1;e2))
20. l : IdLnk
21. n :
||sends(l;<e1,e2>)||
22. t' :
23. e2+1
t'
24. t :
25. <destination(l),t>
E
26.
isnull(a(destination(l);t))
27. isrcv(kind(a(destination(l);t)))
28. ||snds(l;e2)||+n+1
||rcvs(l;t')||
29. lnk(kind(a(destination(l);t))) = l
30. ||rcvs(l;t)|| = ||snds(l;e2)||+n
31. True
32. lnk(kind(a(destination(l);t))) = l
33. isrcv(kind(<destination(l),t>))
34. match(l;e2;t)
35.
source(l) = e1
36. onlnk(l;m(e1;e2)) = nil
source(l) = e1
