[Solved]: Lambda Calculus Evaluation

The reason that $(lambda y. lambda x. lambda y.y) (lambda x. lambda y. y)$ reduces to $lambda x. lambda y. y$ and not to $lambda x. lambda y.lambda x.lambda y.y$ is that the $y$ in the body of $lambda y.lambda x.lambda y.y$ refers to the argument of the third lambda, not the first. If you rename the arguments to have distinct names, $lambda y.lambda x.lambda y.y$ would be written as $lambda y_1.lambda x.lambda y_2.y_2$. So if you apply that function to the argument, that means that every occurrence of $y_1$ in $lambda x.lambda y_2.y_2$ should be replaced with the argument. However $y_1$ does not appear at all in that expression, so the argument is simply ignored and the result is just $lambda x.lambda y_2.y_2$.