GenAutomata
Sections
NuprlLIB
Doc
Def
send-enabledR(E)(L_1,L_2) ==
x:|E|.
(is-send(E)(x)) & L_2 = (L_1 @ [x])
is mentioned
In prior sections:
mb
hybrid
GenAutomata
Sections
NuprlLIB
Doc
x:|E|. 
(is-send(E)(x)) & L_2 = (L_1 @ [x])