mb
structures
Sections
GenAutomata
Doc
Def
tag(E) == 1of(2of(2of(2of(2of(2of(E))))))
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
< tr > _tg == filter(
e.tag(E)(e) =
tg;tr)
[tag_sublist]
Try larger context:
GenAutomata
mb
structures
Sections
GenAutomata
Doc