is mentioned by

Thm* E:TaggedEventStruct, tr:|E| List, i:||tr||. (tr[i] < tr > _tag(E)(tr[i]))	[tag_sublist_member_trivial]
Def No-dup-send(E)(tr) == i,j:||tr||. (is-send(E)(tr[i])) (is-send(E)(tr[j])) (tr[i] =msg=(E) tr[j]) i = j	[no_duplicate_send]

In prior sections: int 1 bool 1 int 2 list 1 mb nat num thy 1 mb list 1 mb list 2 prog 1 mb basic

Try larger context: GenAutomata