Substitution

Remarks

Usually $\theta(x) = x$ for all but finitely many $x$, and $\theta$ is written $\set{x_1 \mapsto s_1, \ldots, x_k \mapsto s_k}$. A term $s$ is an instance of $t$ if $s = t\theta$ for some substitution $\theta$. The substitutions are exactly the endomorphisms of the term algebra $T(X)$, restricted to the variables. For an identity $s \approx t$, the identity $s\theta \approx t\theta$ holds in every algebra in which $s \approx t$ holds.

Example: with $\theta = \set{x \mapsto z \cdot z, \ y \mapsto 1}$, clause 3 and clause 1 give $(x + y)\theta = (z \cdot z) + 1$.

Non-example: the replacement of the first occurrence of $x$ in $x + x$ by $y$ is not a substitution. By clauses 1 and 3, every substitution sends $x + x$ to $\theta(x) + \theta(x)$, which never equals $y + x$.