E:EventStruct. safetyR(E) preserves No-dup-deliver(E)E:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P 
safetyR(E) preserves P| Rank | Theorem | Name |
| 3 |
Thm* E:EventStruct. safetyR(E) preserves No-dup-deliver(E) | [P_no_dup_deliver_safety] |
| cites | ||
| 2 |
Thm* E:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P safetyR(E) preserves P | [strong_safety_implies_safety] |