Past exam of the year 1 of the computer science course of the University of Oxford / 2022 / Digital systems, linear algebra, introduction to formal proof / 8 / f / ii

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, andThe 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.