Thm* E:EventStruct, P:((Label![](FONT/dash.png) (|E| List))![](FONT/dash.png) Prop).
( f,g:(Label![](FONT/dash.png) (|E| List)). ( p:Label. g(p) f(p)) ![](FONT/eq.png) P(f) ![](FONT/eq.png) P(g)) ![](FONT/eq.png)
( f,g:(Label![](FONT/dash.png) (|E| List)).
( a:|E|. p:Label. g(p) = filter( b.![](FONT/not.png) (b =msg=(E) a);f(p))) ![](FONT/eq.png) P(f) ![](FONT/eq.png) P(g))
![](FONT/eq.png)
( f,g,h:(Label![](FONT/dash.png) (|E| List)).
( p,q:Label. ( x f(p).( y g(q). (x =msg=(E) y)))) ![](FONT/eq.png)
( p:Label. h(p) = ((f(p)) @ (g(p)))) ![](FONT/eq.png) P(f) ![](FONT/eq.png) P(g) ![](FONT/eq.png) P(h))
![](FONT/eq.png)
switchable0(E)(local_deliver_property(E;P)) | [local_deliver_switchable] |