E:EventStruct. R_strong_safety(E) preserves No-dup-deliver(E)k,m:
, f:(k
m). increasing(f;k) 
Inj(k; m; f)| Rank | Theorem | Name |
| 2 |
Thm* E:EventStruct. R_strong_safety(E) preserves No-dup-deliver(E) | [P_no_dup_strong_safety] |
| cites | ||
| 1 |
Thm* k,m:, f:(km). increasing(f;k) Inj(k; m; f) | [increasing_inj] |