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] |