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)?