# Applied $\pi$-calculus: Name binding and if clauses

Assume in the applied pi-calculus we have the following process: $$(\nu n)\overline{c} \langle n \rangle.0 | (\nu n) (c(y).(\text{if n=y then P else Q}))$$ where $$P$$ and $$Q$$ are further processes.

I know that the following reduction semantic holds for the applied $$\pi$$-calculus (from wikipedia): $$\overline{x}\langle z \rangle.P | x(y).Q \rightarrow P | Q[z/y]$$ where $$Q[z/y]$$ denotes the process $$Q$$ in which the free name $$z$$ has been ”substituted” for the free occurrences of $$y$$. If a free occurrence of $$y$$ occurs in a location where $$z$$ would not be free, alpha-conversion may be required.

Do I understand correctly, that in the above example, because $$n$$ is already used and thus not free, we would need to rename and thus the reduction would be like so: $$(\nu n’) (\nu n) (c(y).(\text{if n=n’ then P else Q}))$$

While on the other hand, in the following process: $$(\nu n)\overline{c} \langle n \rangle.0 | c(y).(\text{if n = y then P else Q}))$$ because $$n$$ is not bound, we can simply perform the transaction like so: $$(\nu n) (\text{if n = n then P else Q})$$ (and thus those two processes are also semantically different)?