(filter(
e.
is-send(E)(e)
loc(E)(e) =
x1;x) @ nil)
=
filter(e.is-send(E)(e)loc(E)(e) = x1;x)
(|E| List))Prop
f,g:(Label(|E| List)). (p:Label. g(p) 
f(p)) 
P(f) P(g)f,g:(Label(|E| List)).
(
a:|E|. p:Label. g(p) = filter(b.(b =msg=(E) a);f(p))) P(f) P(g)f,g,h:(Label(|E| List)).
(p,q:Label. (x
f(p).(yg(q).(x =msg=(E) y))))
(p:Label. h(p) = ((f(p)) @ (g(p)))) P(f) P(g) P(h)p.x delivered at p) x @ [x@0] delivered at x1 = x delivered at x1| 1 | 13. is-send(E)(x@0) (filter(e.is-send(E)(e)loc(E)(e) = x1;x) @ nil)
=
filter(e.is-send(E)(e)loc(E)(e) = x1;x) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |