3.2.2 Substitutions

We use the notation $P[E/x]$ for a substitution of all free occurrences of the variable $x$ in $P$ by the expression $E$. Several substitutions can be performed simultaneously with $P(E_1/x_1,\ldots ,E_ n/x_ n)$. In particular, we use the syntax $P[\mathbf{x}’/\mathbf{x}]$ to denote the substitution of each identifier $x$ in the sequence $\mathbf{x}$ by $x’$. For more information on free identifiers, see Section 3.3.1.3.

Examples: