mb hybrid Sections GenAutomata Doc

Def Macro x R_del(E) y == (x =msg=(E) y) & is-deliver(E)(x) & (is-send(E)(y)) (is-send(E)(x)) & is-deliver(E)(y)

is not mentioned in this or prior sections.

Try larger context: GenAutomata

mb hybrid Sections GenAutomata Doc