is mentioned by

Thm* E:TaggedEventStruct, tr:|E| List, i:||tr||. (tr[i] < tr > _tag(E)(tr[i]))	[tag_sublist_member_trivial]
Thm* E:TaggedEventStruct, tr:|E| List, x:|E|, t:Label. (x < tr > _t) (x tr) & tag(E)(x) = t	[member_tag_sublist]
Thm* E:TaggedEventStruct. tag(E) |E|Label	[event_tag_wf]
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)	[event_msg_eq_equiv]
Thm* E:EventStruct. is-send(E) |E|	[event_is_snd_wf]
Thm* E:EventStruct. loc(E) |E|Label	[event_loc_wf]
Thm* E:EventStruct. msg(E) |E||MS(E)|	[event_msg_wf]
Thm* M:MessageStruct. EquivRel(|M|)(_1 =(M) _2)	[msg_eq_equiv]
Thm* M:MessageStruct. uid(M) |M|	[msg_id_wf]
Thm* M:MessageStruct. sender(M) |M|Label	[msg_sender_wf]
Thm* M:MessageStruct. content(M) |M||cEQ(M)|	[msg_content_wf]
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]

In prior sections: core fun 1 well fnd int 1 bool 1 rel 1 sqequal 1 int 2 list 1 prog 1 mb basic mb nat union num thy 1 mb list 1 mb label mb list 2

Try larger context: GenAutomata