Restrizione e re-etichettatura su CCS

Question

In un processo come $$ r stackrel {def} = ((a. Bar {b} .0) setminus {b }) [a a b] mid ( bar {b} .b. 0)+ bar {b} .c.0 $$

$ b $ è limitato all'esecuzione del processo interno di rhs $ (a. bar {b} .0) setminus {b } $, da allora in poi $ a $ viene riempito a $ b $. Quello che sono confuso è nel disegnarlo, l'azione $ a $ si verifica al primo processo (possiamo avere una transizione con l'etichetta $ a $ in LTS) ed è il prossimo processo che si svolge la ridenominazione? I seguenti LT possono essere validi come prime azioni transizioni? (La barra è sostituita da sottolineatura)