is mentioned by

Thm* E:EventStruct. (ternary) composableR(E) preserves No-dup-deliver(E)	[P_no_dup_composable]
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]

In prior sections: mb nat

Try larger context: GenAutomata