However, due to the above remark, the
bound variables of a term do not get affected by a replacement,
therefore, it makes sense to introduce a replacement operation, which
we call ``parallel replacement'', in which no canonicalization and
$\alpha$-renaming steps are intermixed with the replacements.  For
example, the parallel replacement of the terms bound to $z_1$ and
$z_2$, where $z_1 \not\equiv z_2$, by $N_1$ and $N_2$ will be written
as $M[z_1 \leftarrow N_1, z_2 \leftarrow N_2]$, and consists of first
replacing $z_1$ and then replacing $z_2$ in $M[z_1 \leftarrow N_1]$,
and not in $\overline{M[z_1 \leftarrow N_1]}$.


\begin{definition}[Parallel replacement]
Given GRS terms $M, N_1$ and $N_2$ in canonical form, $z_1, z_2 \in {\tt BV}(M)$
and $z_1 \not\equiv z_2$, 
the replacement of the terms bound to $z_1$ and $z_2$
in $M$ by $N_1$ and $N_2$, written as
$M[z_1 \leftarrow N_1, z_2 \leftarrow N_2]$, is 
$\{ x_1=e_1; \cdots ;x_i=N_1; \cdots x_j = N_2; \; x_p=e_p; \;\; {\sf In} \; x \}$,
where $x_i \equiv z_1$ and $x_j \equiv z_2$.
\end{definition}


The name ``parallel replacement '' is due to the following observation:

\begin{remark}
\label{parallelreplacement}
Given GRS terms $M$, $N_1$ and $N_2$ in canonical form
such that
$z_1, z_2 \in {\tt BV}(M)$, and $z_1 \not\equiv z_2$,
$$M[z_1 \leftarrow N_1,z_2 \leftarrow N_2] \equiv
  M[z_2 \leftarrow N_2,z_1 \leftarrow N_1].$$
\end{remark}

