Free for substitution
= Free for substitution
A <first-order term> $\tau$ is <free for substitution> for a variable $z$ in a <first-order formula> when no <free variable> of $\tau$ becomes bound after replacing a free occurrence of $z$. Equivalently, at every free occurrence to be replaced, none of its enclosing <quantifiers> binds a variable appearing in $\tau$. The test depends on occurrences and scopes, not merely on which variable names appear anywhere in the formula.