Is (λx.FV(A)) and (λx.FV(B)) β-equivalent?
Free variables have a &quot;meaning&quot; in the sense that two free variables (as opposed to two bound variables) are not $\alpha$-equivalent -- and that's precisely why your first reduction is not correct: We are not allowed to do &quot;free renaming&quot;, only bound renaming!
Capture avoiding substitution is defined as

If $x \neq y$ and $y \in FV(N)$ and $x \in FV(P)$, then, where $z \not \in FV(N) \cup FV(P)$:
$(\lambda y.P)[N/x] = \lambda z.(P[z/y][N/x])$

Capture avoiding substitution happens only when a variable occurring free in $N$ is bound by lambda abstraction in the term to substitute ($y \in FV(N)$) and there are actual occurrences of $x$ in $P$ to substitute ($x \neq y$ and $x \in FV(P)$). In that case, we rename the bound variable in the term that undergoes substitution (the function body), i.e. $(\lambda y.P) \rightsquigarrow \lambda z. (P[z/y])$, then perform the actual substitution of $N$ for $x$ in $P'$. We do not rename free variables, and we do not perform renaming in the argument.
In your example, beta-reducing $(λx.λz.y x) y$ means to replace every free occurrence of $x$ in $\lambda z. yx$ by $y$ provided that $y$ is free to substitute. y will not be captured by anything: As you observe, $y$ is free in $\lambda z.yx$, and that's precisely why there is no capturing and thus no capture avoiding to perform, and the substitution can be done directly. Thus the correct reduction is

$\newcommand{\bred}{\triangleright_\beta}
\phantom{\triangleright_\beta} (\lambda x. \lambda z. yx)y\\
\bred (\lambda z.yx)[y/x]\\
= \lambda z. (yx[y/x])\\
= \lambda z. (y[y/x])(x[y/x])\\
= \lambda z. yy$

De Bruijn indexing on this term is vacuous, because there are no pairs of binding and bound variables ($\lambda z$ does not bind any occurrences of $z$, and the two occurrences of $y$ are not bound by any abstraction $\lambda y$).

A case where capture avoiding substitution would be needed is if the argument $y$ were bound in the function body, e.g. if instead of the vacuous abstraction $\lambda z$ there were $\lambda y$:

$(\lambda x. \lambda y. yx)y\\
\bred (\lambda y.yx)[y/x]\\
= \lambda z. (yx[z/y][y/x]) \quad \text{(avoiding catpure of $y$)}\\
= \lambda z. (zx[y/x])\\
= \lambda z. zy$


Re. notation and implementation:
It depends a bit on how you define it, but the way I used it above (which is the approach chosen in e.g. Hindley &amp; Seldin (see below):
When bound renaming has to happen to avoid variable capture, then this is part of the definition of substitution, i.e. the result of $(\lambda y.P)[N/x]$ with $y$ free in $N$ syntactically identical (&quot;$=$&quot;, rather than just $\alpha$-equivalent) to $\lambda z.P[z/y][N/x]$.
To express $\alpha$-equivalence in the sense that a pair of terms only differs in their bound variable names, you can write $\equiv_\alpha$.
Alternatively, one could define beta reduction such that substitution can only be performed if no variable conflict occurs, and if it does, one has to prepend a step of $\alpha$-renaming before $\beta$-reducing.
&quot;not $FV(A) \cup FV(B)$&quot; is just the set-theoretic complement relative to the set of all variables, $VAR - (FV(A) \cup FV(B))$. To implement a choice of &quot;the first variable not in $FV(A) \cup FV(B)$&quot; you need to presuppose an ordering of variables such as $x &lt; y &lt; z &lt; x_1 &lt; ... x_n$ and then do something like $min\{x: x \in VAR \land x \not \in FV(A) \land x \not \in FV(B)\}$. The set of free and bound variables is defined by straightforward recursion on the structure of the lambda term.
Furthermore, for a precise notation in the implementation one may want to distinguish between an atomic beta reduction/variable renaming step vs. reducibility/equivalence through a chain of reductions/renamings, as well as $\beta$-reducibility monotonously downwards from $A$ to $B$ as opposed to $\beta$-equivalence by finding a common term both reduce to.
For variables you should use $x, y, z, u, v, w, x_1, x_2, \ldots$; wheras $a, b, c, \ldots$ are more typically understood as constants.
Constants is also what objects and functions interpreted &quot;by context&quot; such as $*, +, sqrt$ would naturally be treated as; their meaning is &quot;fixed from the outside&quot; and you can combine lambda reduction with custom inference steps like $(\lambda x.+xx)(2) \bred +22 =_\mathbb{N} 4$.
You can find the notation I used and all the definitions necessary for rigorously implementing substitution etc. in (amongst others)
J. R. Hindley &amp; J.P. Seldin (2008), Lambda calculus and combinators: an introduction.
Another classic is
H. Barendregt (1992), Lambda calculi with types.