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, 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] |