$\beta$ - conversion and $\alpha$-reduction problem in $\lambda$-calculus

Question

Here is an expression that I am trying to reduce and my operations so far:

$$((\lambda x.(x (\lambda z.zy))) (\lambda z.\lambda y. zy) )= (x (\lambda z.zy))[x \to \lambda z.\lambda y. zy ] = ((\lambda z.\lambda y. zy) (\lambda z.zy)) = ((\lambda s.\lambda y. zy) (\lambda z.zy)) = \lambda y. zy$$

Is this procedure correct or am I making some small (or maybe big) mistake?

Thank you very much in advance for your comments.

Answer 1

My result is different:

(λx.(x(λz.zy)))(λz.λy.zy)
(x(λz.zy))[x:=(λz.λy.zy)]
(λz.λd.zd)(λz.zy) //rename z and y so capturing is avoided during substitution
(λz.λd.zd)(λv.vy) 
(λd.zd)[z:=(λv.vy)]
(λd.(λv.vy)d)
(λd.dy)

I think you incorrectly renamed z to s.

Answer 2

$(\lambda z. \lambda y. zy) (\lambda z.zy)$
Before doing the $\beta$-reduction, $y$ is free in the term $\lambda z.zy$, while the name $y$ is bound inside the abstraction on the left, so we change that name on the left.
$(\lambda z. \lambda s. zs) (\lambda z.zy)$
Now we can do the $\beta$-reduction
$\lambda s. (\lambda z.zy) s$
Another $\beta$-reduction
$\lambda s. sy$