is mentioned by

Thm* E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P memorylessR(E) preserves P	[strong_safety_implies_memoryless]
Thm* E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P safetyR(E) preserves P	[strong_safety_implies_safety]
Thm* E:EventStruct. R_strong_safety(E) preserves No-dup-deliver(E)	[P_no_dup_strong_safety]

Try larger context: GenAutomata