is mentioned by

Def tag(E) == 1of(2of(2of(2of(2of(2of(E))))))	[event_tag]
Def is-send(E) == 1of(2of(2of(2of(2of(E)))))	[event_is_snd]
Def loc(E) == 1of(2of(2of(2of(E))))	[event_loc]
Def msg(E) == 1of(2of(2of(E)))	[event_msg]
Def MS(E) == 1of(2of(E))	[event_msg_str]
Def uid(MS) == 1of(2of(2of(2of(2of(MS)))))	[msg_id]
Def sender(MS) == 1of(2of(2of(2of(MS))))	[msg_sender]
Def content(MS) == 1of(2of(2of(MS)))	[msg_content]
Def cEQ(MS) == 1of(2of(MS))	[msg_content_eq]
Def =(DE) == 1of(2of(DE))	[eq_dequiv]
Def |S| == 1of(S)	[carrier]

In prior sections: core mb list 1 prog 1

Try larger context: GenAutomata