GenAutomata
Sections
NuprlLIB
Doc
Def
switchR(tr)(i,j) ==
(is-send(E)(tr[i])) &
(is-send(E)(tr[j])) & i < j & tr[j] somewhere delivered before tr[i]
j < i & tr[i] somewhere delivered before tr[j]
is mentioned
In prior sections:
mb
hybrid
GenAutomata
Sections
NuprlLIB
Doc
(is-send(E)(tr[i])) & (is-send(E)(tr[j])) & i < j & tr[j] somewhere delivered before tr[i] 
j < i & tr[i] somewhere delivered before tr[j]