| Rank | Theorem | Name |
| 6 |
Thm*  E:EventStruct. layerR(E)^-1 preserves No-dup-send(E) | [no_duplicate_send_layer] |
| cites |
| 0 |
Thm* P:(T  Prop), R:(TTProp). R preserves P   R^* preserves P | [preserved_by_star] |
| 3 |
Thm* E:EventStruct. delayableR(E) preserves No-dup-send(E) | [no_duplicate_send_delayable] |
| 3 |
Thm* E:EventStruct. asyncR(E) preserves No-dup-send(E) | [no_duplicate_send_async] |
| 0 |
Thm* P:(TProp), R1,R2:(TTProp).
R1 preserves P R2 preserves P R1  R2 preserves P | [preserved_by_or] |
| 1 |
Thm* E:EventStruct. safetyR(E) preserves No-dup-send(E) | [no_duplicate_send_safety] |
| 0 |
Thm* l1,l2,l3:T List. l1  l2 l1 l2 @ l3 | [iseg_append] |
| 0 |
Thm* P:(TProp), R1,R2:(TTProp).
(x,y:T. (x R1 y) (x R2 y)) R2 preserves P R1 preserves P | [preserved_by_monotone] |
| 2 |
Thm* R1,R2:(TTProp), x,y:T. R1 = > R2 (x (R1^*) y) (x (R2^*) y) | [rel_star_monotonic] |
| 5 |
Thm* E:EventStruct, x,y:|E| List.
(x delayableR(E) y) (y delayableR(E) x) | [R_delayable_symmetric] |
| 5 |
Thm* E:EventStruct, x,y:|E| List. (x asyncR(E) y) (y asyncR(E) x) | [R_async_symmetric] |