mb structures Sections GenAutomata Doc

Def No-dup-send(E)(tr) == i,j:||tr||. (is-send(E)(tr[i])) (is-send(E)(tr[j])) (tr[i] =msg=(E) tr[j]) i = j

is not mentioned in this or prior sections.

Try larger context: GenAutomata

mb structures Sections GenAutomata Doc