is mentioned by

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]
Def < A,evt,tg > (E) == < A,MS(E),msg(E) o evt,loc(E) o evt,is-send(E) o evt,tg, >	[induced_tagged_event_str]
Def induced_event_str(E;A;f) == < A,MS(E),msg(E) o f,loc(E) o f,is-send(E) o f, >	[induced_event_str]
Def Macro is-deliver(E)(x) == (is-send(E)(x))	[event_is_deliver]

Try larger context: GenAutomata