| Rank | Theorem | Name |
| 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] |
| cites |
| 8 |
Thm* E:TaggedEventStruct, P:TraceProperty(E).
switchable(E)(P) ((switch_inv(E)  No-dup-send(E)) fuses P) | [switch_inv_theorem2] |
| 3 |
Thm* E:EventStruct, P:((|E| List)Prop), A:Type, f:(A|E|)
, t:(ALabel). switchable(E)(P) switchable( < A,f,t > (E))(P o f) | [switchable_induced_tagged] |
| 1 |
Thm* E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), tr_l:A List.
No-dup-send(E)(map(evt;tr_l)) No-dup-send( < A,evt,tg > (E))(tr_l) | [no_dup_send_induced] |