is mentioned by

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. tag_splitable(E;adR(E))	[tag_sublist_layer]

Try larger context: GenAutomata