= Solution
\b[The term $x+z$ is <free for substitution> for $z$.] The only free occurrence of the target $z$ is in the outside disjunct $y<z$, beyond both <quantifier> scopes. The occurrences under $\forall z$ are <bound variables> and are not replaced. Therefore no renaming is required, and
$$
\boxed{\varphi[x+z/z]=\bigl(\exists x\,(x<y\to\forall z\,(x<z+2))\bigr)\lor\bigl(y<x+z\bigr).}
$$
The new $x$ and $z$ in the last disjunct are free. <First-order substitution> replaces the original free occurrences once; it does not recursively substitute into the inserted term.
Back to article page
