(Label(|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(p.x delivered at p)

x swap adjacent[loc(E)(x) = loc(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;y) = filter(e.is-send(E)(e)loc(E)(e) = x1;x)

Using [`f',(e.is-send(E)(e)loc(E)(e) = x1)] (FwdThru Thm* P:(AAProp), f:(A), L1,L2:A List. (L1 swap adjacent[P(x,y)] L2) (filter(f;L1) swap adjacent[P(x,y)] filter(f;L2)) filter(f;L1) = filter(f;L2) [-2])
THEN
Analyze -1

1	11. filter(e.is-send(E)(e)loc(E)(e) = x1;x) swap adjacent[loc(E)(x) = loc(E)(y) & is-send(E)(x) & is-send(E)(y) is-send(E)(x) & is-send(E)(y)] filter(e.is-send(E)(e)loc(E)(e) = x1;y) filter(e.is-send(E)(e)loc(E)(e) = x1;y) = filter(e.is-send(E)(e)loc(E)(e) = x1;x)

About: