Thm* E:EventStruct, P:TraceProperty(E), A:Type, evt:(A |E|)
, tg:(A Label), 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: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] |
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] |
Def I fuses P == tr:Trace(E). ( m:Label. P( < tr > _m))  I(tr)  P(tr) | [fusion_condition] |
Def single-tag-decomposable(E)(L)
== L = nil |E| List 
( L_1,L_2:Trace(E).
L = (L_1 @ L_2) |E| List
& L_2 = nil |E| List
& ( x L_1.( y L_2. (x =msg=(E) y)))
& ( m:Label. ( x L_2.tag(E)(x) = m))) | [single_tag_decomposable] |