(is-send(E)(a)) 
(is-send(E)(b)) (a =msg=(E) b)) & ((is-send(E)(a)) (is-send(E)(b)) (
x,y:
||tr||. x < y & (is-send(E)(tr[x])) & (is-send(E)(tr[y])) & (tr[x] =msg=(E) b) & (tr[y] =msg=(E) a)) loc(E)(a) = loc(E)(b))
is mentioned
In prior sections: mb hybrid