I am trying to wrap my head around substitution in lambda calculus and not sure if I am heading in the right direction.
For example,
$[(\lambda y.xy)/x](x(\lambda x.yx))$
Here, we must substitute all free variables of $x$ in the right lambda expression with $\lambda y.xy$.
First, we need to establish the free variables in the right lambda expression.
Since the first $x$ is not preceded by a $\lambda x$, we consider it to be a free variable. Since the other $x$ is preceded by $\lambda x$, it is a bounded variable. The only $y$ variable is free as it is not preceded by a $\lambda y$.
Now, we can substitute for the free variables.
$(\lambda y.xy) (\lambda x.yx)$
Am I heading in the right direction?