is mentioned by

Def tr delivered at p == filter(e.is-send(E)(e)loc(E)(e) = p;tr)	[deliveries_at]
Def (L -msg(a;b) L1) == filter(a.reduce(b,y. msg(a;b)y;true;L1);L)	[remove_msgs]

In prior sections: bool 1 mb list 1 mb list 2 mb basic mb structures mb automata 1

Try larger context: GenAutomata