is mentioned by

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:EventStruct, x,y:|E| List. (x asyncR(E) y) (y asyncR(E) x)	[R_async_symmetric]
Thm* E:EventStruct, P:TraceProperty(E). R_permutation(E) preserves P asyncR(E) preserves P	[permutable_implies_async]
Thm* E:EventStruct. asyncR(E) preserves No-dup-send(E)	[no_duplicate_send_async]
Def adR(E) == (delayableR(E) asyncR(E))^*	[R_ad]
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 layerR(E) == ((asyncR(E) delayableR(E)) send-enabledR(E))^*	[layer_rel]

Try larger context: GenAutomata