mb structures Sections GenAutomata Doc

Def msg(E) == 1of(2of(2of(E)))

is mentioned by

Def =msg=(E)(e_1,e_2) == (msg(E)(e_1)) =(MS(E)) (msg(E)(e_2))[event_msg_eq]
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]

Try larger context: GenAutomata

mb structures Sections GenAutomata Doc