is mentioned by

Thm* E:EventStruct, tr:|E| List. No-dup-deliver(E)(tr) (x,y:|E|. is-send(E)(x) is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr))	[P_no_dup_iff]
Def R_strong_safety(E)(tr_1,tr_2) == sublist(|E|;tr_2;tr_1)	[R_strong_safety]

In prior sections: mb list 1 mb list 2

Try larger context: GenAutomata