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) | [switch_inv_theorem] |
Thm* E:TaggedEventStruct, P:TraceProperty(E).
MCS(E)(P) 
(P refines (Causal(E) No-dup-deliver(E))) 
(((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P) | [switch_inv_plus_normal] |
Thm* E:TaggedEventStruct.
(switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E) | [strong_switch_inv_decomposable] |
Thm* E:TaggedEventStruct, P,I:TraceProperty(E).
MCS(E)(P)  safetyR(E) preserves I  (I refines single-tag-decomposable(E))  (I fuses P) | [M_DASH_C_DASH_S_SPACE_induction] |
Thm* E:TaggedEventStruct.
(switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E))
refines single-tag-decomposable(E) | [switch_decomp_implies_single_tag_decomp] |
Thm* E:TaggedEventStruct, P,I:((|E| List) Prop).
(P refines (Causal(E) No-dup-deliver(E))) 
((I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P) 
((I No-dup-send(E)) fuses P) | [no_DASH_dup_DASH_fusion] |
Thm* E:TaggedEventStruct, P,I:((|E| List) Prop).
(P refines Causal(E)) 
((I No-dup-send(E) Tag-by-msg(E)) fuses P)  ((I No-dup-send(E)) fuses P) | [tag_by_msg_fusion_lemma] |
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E).
((I J) fuses P)  (I fuses J)  (P refines J)  (I fuses P) | [fusion_simplification] |
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E).
(J refines I)  (I fuses P)  (J fuses P) | [fusion_weakening] |
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)) | [tr_refines_and] |
Def switchable(E)(P)
== safetyR(E) preserves P
& memorylessR(E) preserves P
& (ternary) composableR(E) preserves P
& send-enabledR(E) preserves P
& asyncR(E) preserves P
& delayableR(E) preserves P
& (P refines Causal(E))
& (P refines No-dup-deliver(E)) | [b_switchable] |