E:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P 
safetyR(E) preserves PL_1,L_2:T List. L_1 
L_2 sublist(T;L_1;L_2)| Rank | Theorem | Name |
| 2 |
Thm* E:EventStruct, P:TraceProperty(E).
R_strong_safety(E) preserves P safetyR(E) preserves P | [strong_safety_implies_safety] |
| cites | ||
| 1 |
Thm* L_1,L_2:T List. L_1 L_2 sublist(T;L_1;L_2) | [iseg_is_sublist] |