(filter(
e.
is-send(E)(e)
loc(E)(e) =
x1;x)[i] 
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. (xf(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 =msg=(E) y) & is-send(E)(x) & is-send(E)(y) 
is-send(E)(x) & is-send(E)(y)] y
(||filter(e.is-send(E)(e)loc(E)(e) = x1;x)||-1)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i]
=msg=(E) filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)])e.is-send(E)(e)loc(E)(e) = x1;x)[i])is-send(E)(filter(e.is-send(E)(e)loc(E)(e) = x1;x)[(i+1)])e.is-send(E)(e)loc(E)(e) = x1;y)
=
swap(filter(e.is-send(E)(e)loc(E)(e) = x1;x);i;i+1)x@0:|E|.
(x@0 filter(e.is-send(E)(e)loc(E)(e) = x1;x)) is-send(E)(x@0) & loc(E)(x@0) = x1 filter(e.is-send(E)(e)loc(E)(e) = x1;y) = filter(e.is-send(E)(e)loc(E)(e) = x1;x)e.is-send(E)(e)loc(E)(e) = x1;x)[i]] -1| 1 | (filter(e.is-send(E)(e)loc(E)(e) = x1;x)[i] filter(e.is-send(E)(e)loc(E)(e) = x1;x)) |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |