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 send-enabledR(E)(L_1,L_2) == x:|E|. (is-send(E)(x)) & L_2 = (L_1 @ [x])	[R_send_enabled]
Def composableR(E)(L_1,L_2,L) == (xL_1.(yL_2.(x =msg=(E) y))) & L = (L_1 @ L_2) |E| List	[R_composable]
Def single-tag-decomposable(E)(L) == L = nil |E| List (L_1,L_2:Trace(E). L = (L_1 @ L_2) |E| List & L_2 = nil |E| List & (xL_1.(yL_2.(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m)))	[single_tag_decomposable]

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

Try larger context: GenAutomata