mb structures Sections GenAutomata Doc

Def < tr > _tg == filter(e.tag(E)(e) = tg;tr)

is mentioned by

Thm* E:TaggedEventStruct, tr:|E| List, i:||tr||. (tr[i] < tr > _tag(E)(tr[i]))[tag_sublist_member_trivial]
Thm* E:TaggedEventStruct, tr:|E| List, x:|E|, t:Label. (x < tr > _t) (x tr) & tag(E)(x) = t[member_tag_sublist]
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]

Try larger context: GenAutomata

mb structures Sections GenAutomata Doc