E:TaggedEventStruct, P:TraceProperty(E). switchable(E)(P) ((switch_inv(E) No-dup-send(E)) fuses P)

Unfold `trace_property` 0
THEN
Unfold `b_switchable` -1
THEN
Reduce -1
THEN
ExRepD
THEN
BackThru Thm* E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) asyncR(E) preserves P delayableR(E) preserves P (P refines (Causal(E) No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P)
THEN
Try (Unfold `trace_property` 0)
THEN
Try (BackThru Thm* E:Structure, P,Q_1,Q_2:((|E| List)Prop). (P refines Q_1) (P refines Q_2) (P refines (Q_1 Q_2)))
THEN
Try ((Unfold `memoryless_composable_safety` 0) THEN (Reduce 0))

None

About: