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. isrcv(lnk(kind(e));a(loc(e);time(e)))
9. destination(lnk(kind(e))) = loc(e)
10. r :
11. ||rcvs(lnk(kind(e));time(e))|| = r
12. ms : Msg
13. msg(a(loc(e);time(e))) = ms
14. l : IdLnk
15. lnk(kind(e)) = l
16. t' :
17. time(e) = t'
18. r<||snds(l;t')||
19. concat(map(
t1.m(l;t1);upto(t')))[r] = ms
20. m :
||map(t1.m(l;t1);upto(t'))||
21. ||concat(firstn(m;map(
t1.m(l;t1);upto(t'))))||r
21. & r-||concat(firstn(m;map(
t1.m(l;t1);upto(t'))))||<||map(t1.
21. m(l;t1);upto(t'))[m]||
21. & concat(map(
t1.m(l;t1);upto(t')))[r]
21. & =
21. & map(
t1.m(l;t1);upto(t'))[m][(r-||concat(firstn(m;map(t1.
21. & m(l;t1);upto(t'))))||)]
m<t'
