is mentioned by

Thm* E:TaggedEventStruct, tr:|E| List, x:|E|, t:Label. (x < tr > _t) (x tr) & tag(E)(x) = t	[member_tag_sublist]
Thm* E:TaggedEventStruct. tag(E) |E|Label	[event_tag_wf]
Thm* E:EventStruct. loc(E) |E|Label	[event_loc_wf]
Thm* M:MessageStruct. sender(M) |M|Label	[msg_sender_wf]
Def tag_splitable(E;R) == tr_1,tr_2:Trace(E). (tr_1 R tr_2) (m:Label. < tr_1 > _m R < tr_2 > _m)	[tag_splitable]
Def TaggedEventStruct == E:TypeM:MessageStruct(E|M|)(ELabel)(E)(ELabel)Top	[tagged_event_str]
Def EventStruct == E:TypeM:MessageStruct(E|M|)(ELabel)(E)Top	[event_str]
Def MessageStruct == M:TypeC:DecidableEquiv(M|C|)(MLabel)(M)Top	[message_str]

In prior sections: mb label

Try larger context: GenAutomata