= Solution
\b[The term $x+z$ is not <free for substitution> for $y$.] The occurrence of $y$ in $x<y$ is under $\exists x$, which would capture the inserted $x$. The other occurrence, in the outside disjunct $y<z$, has no enclosing <quantifier>. The inner $\forall z$ does not bind the occurrence of $y$ in its antecedent, so it creates no additional capture at that substitution site.
Rename the bound $x$ to a fresh $u$, then carry out <capture-avoiding first-order substitution>. The result is
$$
\boxed{\varphi[x+z/y]=\bigl(\exists u\,(u<x+z\to\forall z\,(u<z+2))\bigr)\lor(x+z<z).}
$$
The inserted $z$ in $u<x+z$ remains free because it lies outside the scope of $\forall z$. One may additionally rename that bound $z$ for readability, but it is not necessary for correctness.
Back to article page
