| Rank | Theorem | Name |
| 10 |
Thm*  E:EventStruct, P:TraceProperty(E), A:Type, evt:(A  |E|)
, tg:(ALabel), tr_u:Trace(E), tr_l:A List.
switchable(E)(P)  
No-dup-send(E)(tr_u)
full_switch_inv(E;A;evt;tg;tr_u;tr_l) (m:Label. P(map(evt; < tr_l > _m))) P(tr_u) | [switch_main_theorem] |
| cites |
| 9 |
Thm* E:EventStruct, P:((|E| List)Prop), A:Type, evt:(A|E|), tg:(ALabel)
, tr:A List.
switchable(E)(P)
No-dup-send(E)(map(evt;tr))
switch_inv( < A,evt,tg > (E))(tr) (m:Label. P(map(evt; < tr > _m))) P(map(evt;tr)) | [switch_theorem] |
| 6 |
Thm* E:EventStruct. layerR(E)^-1 preserves No-dup-send(E) | [no_duplicate_send_layer] |
| 6 |
Thm* E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), m:Label
, tr1,tr2:A List. (tr1 R(tg) tr2) < tr1 > _m = < tr2 > _m  A List | [tag_sublist_preserved] |
| 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] |