GenAutomata Sections NuprlLIB Doc

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

is mentioned

In prior sections: mb hybrid


GenAutomata Sections NuprlLIB Doc