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'])))
is not mentioned in this or prior sections.
Try larger context: GenAutomata