is mentioned by

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, tr:|E| List. (m:Label. Causal(E)( < tr > _m)) No-dup-send(E)(tr) Tag-by-msg(E)(tr)	[P_tag_by_msg_lemma]

Try larger context: GenAutomata