7. y: |E| List
8. P(
p.x delivered at p)9. x@0: |E|
10. is-send(E)(x@0)
11. y = (x @ [x@0])
P(p.x @ [x@0] delivered at p)
(|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) send-enabledR(E) preserves tr.P(p.tr delivered at p)| 1 | 6. x: |E| List 7. y: |E| List 8. P( p.x delivered at p)9. x@0: |E| 10. is-send(E)(x@0) 11. y = (x @ [x@0]) P(p.x @ [x@0] delivered at p) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |