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] |
|
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] |
Thm* E:TaggedEventStruct, P:TraceProperty(E).
switchable(E)(P) ((switch_inv(E)  No-dup-send(E)) fuses P) | [switch_inv_theorem2] |
|
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] |
|
Thm* E:EventStruct.
switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E)) | [totalorder_switchable] |
|
Thm* E:EventStruct, A:Type, f:(A|E|), P:((|E| List)Prop).
switchable(E)(P) switchable(induced_event_str(E;A;f))(P o f) | [switchable_induced] |
|
Thm* E:EventStruct, P:TraceProperty(E).
switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E)) | [switchable0_switchable] |