E:EventStruct. R_permutation(E) preserves No-dup-deliver(E)k:
, i,j:k. (i, j) 
k
kL:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| 
k:, i,j:k. Bij(k; k; (i, j))| Rank | Theorem | Name |
| 3 |
Thm* E:EventStruct. R_permutation(E) preserves No-dup-deliver(E) | [P_no_dup_permutable] |
| cites | ||
| 0 | Thm* k:, i,j:k. (i, j) kk | [flip_wf] |
| 2 |
Thm* L:T List, i,j:||L||. ||swap(L;i;j)|| = ||L|| | [swap_length] |
| 0 |
Thm* k:, i,j:k. Bij(k; k; (i, j)) | [flip_bijection] |