is mentioned by

Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)	[event_msg_eq_equiv]
Thm* M:MessageStruct. EquivRel(|M|)(_1 =(M) _2)	[msg_eq_equiv]
Thm* E:DecidableEquiv. EquivRel(|E|)(_1 =(E) _2)	[eq_dequiv_equiv]
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 tag_splitable(E;R) == tr_1,tr_2:Trace(E). (tr_1 R tr_2) (m:Label. < tr_1 > _m R < tr_2 > _m)	[tag_splitable]
Def =msg=(E)(e_1,e_2) == (msg(E)(e_1)) =(MS(E)) (msg(E)(e_2))	[event_msg_eq]
Def =(M)(m_1,m_2) == ((content(M)(m_1)) =(cEQ(M)) (content(M)(m_2)))sender(M)(m_1) = sender(M)(m_2) (uid(M)(m_1)=uid(M)(m_2))	[msg_eq]
Def DecidableEquiv == T:TypeE:TTEquivRel(T)((_1 E _2))Top	[dequiv]

In prior sections: mb basic mb nat mb list 1 mb list 2 rel 1

Try larger context: GenAutomata