2. e : E
3.
i:Id, t:
, l:IdLnk. 
source(l) = i 
onlnk(l;m(i;t)) = nil
4.
i:Id, t:. isnull(a(i;t)) (x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
5.
i:Id, t:, l:IdLnk.
5. isrcv(l;a(i;t))
5.
5. destination(l) = i & ||queue(l;t)||
1 & hd(queue(l;t)) = msg(a(i;t))
6.
l:IdLnk, t:.
6.
t':. t
t' & isrcv(l;a(destination(l);t')) 
queue(l;t') = nil
7. isrcv(kind(e))
8.
n:. match(lnk(kind(e));n;time(e))
9. t :
10. l : IdLnk
11. ||onlnk(l;m(source(l);t))||
12. ||snds(l;t)||
||rcvs(l;time(e))||
13. ||rcvs(l;time(e))||<||snds(l;t)||+||onlnk(l;m(source(l);t))||
14. isnull(a(source(l);t))
15.
x:Id. s(source(l);t+1).x = s(source(l);t).x
16. m(source(l);t) = nil
False
