is mentioned by
Thm* E:EventStruct, P:TraceProperty(E). switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E)) | [switchable0_switchable] |
Thm* E:EventStruct. switchable0(E)(totalorder(E)) | [totalorder_switchable0] |
Thm* E:EventStruct. switchable0(E)(No-dup-deliver(E)) | [P_no_dup_switchable0] |
Thm* E:EventStruct. switchable0(E)(Causal(E)) | [P_causal_switchable0] |
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] |
Try larger context: GenAutomata