| Rank | Theorem | Name |
| 6 |
Thm*  E:TaggedEventStruct, P:TraceProperty(E).
MCS(E)(P)  
(P refines (Causal(E)  No-dup-deliver(E)))
(((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P) | [switch_inv_plus_normal] |
| cites |
| 0 |
Thm* P,Q:(T  Prop), R:(TTProp).
R preserves P R preserves Q R preserves P Q | [and_preserved_by] |
| 3 |
Thm* E:TaggedEventStruct.
(switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E))
refines single-tag-decomposable(E) | [switch_decomp_implies_single_tag_decomp] |
| 5 |
Thm* E:TaggedEventStruct.
(switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E) | [strong_switch_inv_decomposable] |