| Rank | Theorem | Name |
| 5 |
Thm*  E:EventStruct, P:TraceProperty(E).
switchable0(E)(P)   switchable(E)(P  Causal(E) No-dup-deliver(E)) | [switchable0_switchable] |
| cites |
| 4 |
Thm* E:EventStruct. switchable0(E)(Causal(E)) | [P_causal_switchable0] |
| 1 |
Thm* E:EventStruct. switchable0(E)(No-dup-deliver(E)) | [P_no_dup_switchable0] |
| 0 |
Thm* P,Q:(T  Prop), R:(TTTProp).
(ternary) R preserves P (ternary) R preserves Q (ternary) R preserves P Q | [and_preserved_by2] |
| 0 |
Thm* P,Q:(TProp), R:(TTProp).
R preserves P R preserves Q R preserves P Q | [and_preserved_by] |