i:
(||tr||-1). (
(is-send(E)(tr[i])) 
(is-send(E)(tr[(i+1)])) (tr[i] =msg=(E) tr[(i+1)])) & ((
x,y:||tr||. x < y & (is-send(E)(tr[x])) & (is-send(E)(tr[y])) & tr[x] delivered at time i+1 & tr[y] delivered at time i) loc(E)(tr[i]) = loc(E)(tr[(i+1)]))
is mentioned
In prior sections: mb hybrid