is mentioned by

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]

In prior sections: fun 1 list 1 mb nat mb list 1 mb list 2

Try larger context: GenAutomata