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
4.
i:Id, t:, l:IdLnk.
4. isrcv(l;a(i;t))
4.
4. destination(l) = i & ||queue(l;t)||
1 & hd(queue(l;t)) = msg(a(i;t))
5.
l:IdLnk, t:.
5.
t':. t
t' & isrcv(l;a(destination(l);t')) 
queue(l;t') = nil
6.
e,e':E. 1of(e) = 1of(e') e <c e' e = e' e' <c e
7.
e:E. first(e) 
(e':E. 1of(e') = 1of(e) e' <c e)
8.
e:E.
8.
first(e)
8.
8. 1of(pred(e)) = 1of(e) & pred(e) <c e
8. & (
e':E. 1of(e') = 1of(e) (pred(e) <c e' & e' <c e))
9.
e:E. first(e) (x:Id. (x when e) = (x after pred(e)))
10. Trans e,e':E. e <c e'
11. SWellFounded(e <c e')
12.
e:E.
12. isrcv(kind(a(1of(e);2of(e))))
12.
12. sends(lnk(kind(a(1of(e);2of(e))));sender(e))[index(e)]
12. =
12. msg(lnk(kind(a(1of(e);2of(e))));tag(kind(a(1of(e);2of(e))));val(e))
13.
e:E. isrcv(kind(a(1of(e);2of(e)))) sender(e) <c e
14.
e,e':E.
14. e <c e'
14.
14.
first(e') & e <c pred(e') e = pred(e')
14.
isrcv(kind(a(1of(e');2of(e')))) & e <c sender(e') e = sender(e')
15.
e:E.
15. isrcv(kind(a(1of(e);2of(e))))
15.
15. 1of(e) = destination(lnk(kind(a(1of(e);2of(e)))))
16. e1 : Id
17. e2 :
18.
isnull(a(e1;e2))
19. l : IdLnk
20.
e1 = source(l)
sends(l;<e1,e2>) = nil 
Msg_sub(l; the_w.M) List
