is mentioned by

Def totalorder(E)(tr) == p,q:Label. agree_on_common(|MS(E)|;map(msg(E);tr delivered at p);map(msg(E);tr delivered at q))

[totalorder]

In prior sections: mb structures

Try larger context: GenAutomata