is mentioned by

Thm* E:EventStruct, P:TraceProperty(E). R_permutation(E) preserves P asyncR(E) preserves P	[permutable_implies_async]
Thm* E:EventStruct, P:TraceProperty(E). R_permutation(E) preserves P delayableR(E) preserves P	[permutable_implies_delayable]
Thm* E:EventStruct. R_permutation(E) preserves No-dup-deliver(E)	[P_no_dup_permutable]

Try larger context: GenAutomata