is mentioned by

Thm* E:EventStruct, P:((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)) switchable0(E)(local_deliver_property(E;P))	[local_deliver_switchable]
Def memorylessR(E)(L_1,L_2) == a:|E|. L_2 = filter(b.(b =msg=(E) a);L_1) |E| List	[R_memoryless]
Def tr delivered at p == filter(e.is-send(E)(e)loc(E)(e) = p;tr)	[deliveries_at]
Def (L -msg(a;b) L1) == filter(a.reduce(b,y. msg(a;b)y;true;L1);L)	[remove_msgs]

In prior sections: mb list 1 mb list 2 mb structures mb events

Try larger context: GenAutomata