| Rank | Theorem | Name |
| 7 |
Thm*  E:TaggedEventStruct, P:TraceProperty(E).
MCS(E)(P)  
asyncR(E) preserves P
delayableR(E) preserves P
(P refines (Causal(E)  No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P) | [switch_inv_theorem] |
| cites |
| 0 |
Thm* E:TaggedEventStruct, P,I,J,K:TraceProperty(E)
, R:(Trace(E)  Trace(E)Prop).
tag_splitable(E;R)
(tr_1,tr_2:Trace(E). (tr_1 R tr_2) (tr_2 R tr_1))
R preserves P
R preserves K
(tr:Trace(E). (I K)(tr) ( tr':Trace(E). I(tr') & J(tr') & (tr R tr')))
(((I J) K) fuses P) ((I K) fuses P) | [normal_form_fusion] |
| 5 |
Thm* E:EventStruct, x,y:|E| List. (x asyncR(E) y) (y asyncR(E) x) | [R_async_symmetric] |
| 5 |
Thm* E:EventStruct, x,y:|E| List.
(x delayableR(E) y) (y delayableR(E) x) | [R_delayable_symmetric] |
| 0 |
Thm* R1,R2:(TTProp).
Sym x,y:T. x R1 y Sym x,y:T. x R2 y Sym x,y:T. x (R1  R2) y | [symmetric_rel_or] |
| 3 |
Thm* R:(TTProp). Sym x,y:T. x R y Sym x,y:T. x (R^*) y | [rel_star_symmetric] |
| 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] |
| 0 |
Thm* P:(TProp), R:(TTProp). R preserves P R^* preserves P | [preserved_by_star] |
| 6 |
Thm* E:TaggedEventStruct, tr:Trace(E).
(switch_inv(E) No-dup-send(E))(tr)
(tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr')) | [switch_normal_exists] |
| 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] |