The <first-order term> $t$ is <free for substitution> for $x_i$ in $\phi$ if, at every free occurrence of $x_i$ to be replaced, no enclosing quantifier binds a variable occurring in $t$. Equivalently, the substitution introduces no <variable capture>. Only free occurrences of $x_i$ are replaced.

Solution

Past exam of the logic and set theory course of the University of Oxford / 2011 / A / 3 / b / i / Solution

 Solution (source code)