i,j,k:
||tr||. i < j 
(is-send(E)(tr[i])) (is-send(E)(tr[j])) 
tag(E)(tr[i]) = tag(E)(tr[j]) (tr[j] =msg=(E) tr[k]) (is-send(E)(tr[k])) (
k':||tr||. k' < k & loc(E)(tr[k']) = loc(E)(tr[k]) & (tr[i] =msg=(E) tr[k']) & (is-send(E)(tr[k'])))
No mentions to report in GenAutomata.