Solution

ID: 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-resit/8/d/solution

The occurrence of in lies under the quantifier . Directly inserting the term would capture its free : the result would make the inserted bound and change the intended dependence on the original free value. Therefore the term is not free for the literal substitution requested.
Perform capture-avoiding first-order substitution by first renaming bound variables to fresh names. Renaming the first binder to is necessary; renaming the second to is optional but makes the result especially clear. These renamings give the equivalent formula . Substituting only the free occurrences of now gives
Both and in the inserted term remain free variables. The original has scope only over its own disjunct and would not capture the inserted in the first disjunct; its optional renaming is not a necessary capture repair. This distinction avoids confusing reuse of a letter elsewhere with binding within the relevant scope.

New to topics? Read the docs here!