is mentioned by

Thm* E:EventStruct. is-send(E) |E|	[event_is_snd_wf]
Def TaggedEventStruct == E:TypeM:MessageStruct(E|M|)(ELabel)(E)(ELabel)Top	[tagged_event_str]
Def EventStruct == E:TypeM:MessageStruct(E|M|)(ELabel)(E)Top	[event_str]
Def DecidableEquiv == T:TypeE:TTEquivRel(T)((_1 E _2))Top	[dequiv]

In prior sections: bool 1 rel 1 sqequal 1 list 1 mb basic mb nat mb list 1 mb list 2 prog 1

Try larger context: GenAutomata