is mentioned by

Thm* E:TaggedEventStruct, P:TraceProperty(E). switchable(E)(P) ((switch_inv(E) No-dup-send(E)) fuses P)	[switch_inv_theorem2]
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]
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]
Thm* E:TaggedEventStruct, P,I:TraceProperty(E). MCS(E)(P) safetyR(E) preserves I (I refines single-tag-decomposable(E)) (I fuses P)	[M_DASH_C_DASH_S_SPACE_induction]
Thm* E:TaggedEventStruct, P,I:((|E| List)Prop). (P refines (Causal(E) No-dup-deliver(E))) ((I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P) ((I No-dup-send(E)) fuses P)	[no_DASH_dup_DASH_fusion]
Thm* E:TaggedEventStruct. Tag-by-msg(E) fuses No-dup-deliver(E)	[no_dup_fusion]
Thm* E:TaggedEventStruct, P,I:((|E| List)Prop). (P refines Causal(E)) ((I No-dup-send(E) Tag-by-msg(E)) fuses P) ((I No-dup-send(E)) fuses P)	[tag_by_msg_fusion_lemma]
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]
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E). ((I J) fuses P) (I fuses J) (P refines J) (I fuses P)	[fusion_simplification]
Thm* E:TaggedEventStruct, I,P,Q:TraceProperty(E). (I fuses P) (I fuses Q) (I fuses (P Q))	[fusion_and]
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E). (J refines I) (I fuses P) (J fuses P)	[fusion_weakening]
Thm* E:TaggedEventStruct. PTrue fuses Causal(E)	[causal_fusion]

Try larger context: GenAutomata