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, 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. (switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E)	[strong_switch_inv_decomposable]
Thm* E:TaggedEventStruct. tag_splitable(E;adR(E))	[tag_sublist_layer]
Thm* E:TaggedEventStruct, tr:|E| List, ls:||tr||. switch_inv(E)(tr) (i,j:||tr||. (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls) tag(E)(tr[i]) = tag(E)(tr[j]))	[switch_inv_rel_closure]
Thm* E:TaggedEventStruct, tr:|E| List. switch_inv(E)(tr) (i,j:||tr||. (i switchR(tr) j) tag(E)(tr[i]) = tag(E)(tr[j]))	[switch_inv_rel_same_tag]
Thm* E:TaggedEventStruct. safetyR(E) preserves switch_inv(E)	[switch_inv_safety]
Thm* E:TaggedEventStruct, x:|E| List, i:(||x||-1). switch_inv(E)(x) is-send(E)(x[(i+1)]) is-send(E)(x[i]) loc(E)(x[i]) = loc(E)(x[(i+1)]) switch_inv(E)(swap(x;i;i+1))	[switch_inv_swap]
Thm* E:TaggedEventStruct. switch_inv(E) (|E| List)Prop	[switch_inv_wf]
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. safetyR(E) preserves AD-normal(E)	[switch_normal_safety]
Thm* E:TaggedEventStruct. (switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E)) refines single-tag-decomposable(E)	[switch_decomp_implies_single_tag_decomp]
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. safetyR(E) preserves Tag-by-msg(E)	[P_tag_by_msg_safety]
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, tr:|E| List, x,y:|E|. Dec(R_ad_normal(tr)(x,y))	[decidable__R_ad_normal]
Thm* E:TaggedEventStruct. PTrue fuses Causal(E)	[causal_fusion]
Thm* E:TaggedEventStruct, tr:|E| List. (m:Label. Causal(E)( < tr > _m)) No-dup-send(E)(tr) Tag-by-msg(E)(tr)	[P_tag_by_msg_lemma]

In prior sections: mb structures

Try larger context: GenAutomata