E:EventStruct. delayableR(E) preserves No-dup-send(E)k:
, i,j:k. Bij(k; k; (i, j))L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| 
| Rank | Theorem | Name |
| 3 |
Thm* E:EventStruct. delayableR(E) preserves No-dup-send(E) | [no_duplicate_send_delayable] |
| cites | ||
| 0 |
Thm* k:, i,j:k. Bij(k; k; (i, j)) | [flip_bijection] |
| 2 |
Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| | [swap_length] |