is mentioned by

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

Try larger context: GenAutomata