E:TaggedEventStruct, tr:|E| List, i:
||tr||.
(tr[i] 
< tr > _tag(E)(tr[i]))E:TaggedEventStruct, tr:|E| List, x:|E|, t:Label.
(x < tr > _t) 
(x tr) & tag(E)(x) = t l) == 
i:. i < ||l|| & x = l[i] T
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] |
In prior sections: mb list 1 mb label mb list 2
Try larger context: GenAutomata