asyncR(E))^* delayableR(E)) send-enabledR(E))^* R2)(x,y) == (x R1 y) (x R2 y)
is mentioned by
|
Def adR(E) == (delayableR(E) asyncR(E))^* | [R_ad] |
|
Def layerR(E) == ((asyncR(E) delayableR(E)) send-enabledR(E))^* | [layer_rel] |
In prior sections: mb nat
Try larger context: GenAutomata