is mentioned by

Thm* E:TaggedEventStruct. safetyR(E) preserves switch_inv(E)	[switch_inv_safety]
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. safetyR(E) preserves AD-normal(E)	[switch_normal_safety]
Thm* E:TaggedEventStruct. safetyR(E) preserves Tag-by-msg(E)	[P_tag_by_msg_safety]
Thm* E:EventStruct. safetyR(E) preserves No-dup-deliver(E)	[P_no_dup_deliver_safety]
Thm* E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P safetyR(E) preserves P	[strong_safety_implies_safety]
Thm* E:EventStruct. safetyR(E) preserves Causal(E)	[P_causal_safety]
Thm* E:EventStruct. safetyR(E) preserves No-dup-send(E)	[no_duplicate_send_safety]
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]
Def switchable0(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	[switchable0]
Def MCS(E)(P) == memorylessR(E) preserves P & (ternary) composableR(E) preserves P & safetyR(E) preserves P	[memoryless_composable_safety]

Try larger context: GenAutomata