# How do we show $\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$ in lambda calculus?

How do we show $$\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x . x)$$?

I was going through the slides here and it asked to do the above but by page 16 of the slides we have not defined what lambda applications are suppose to be. Thus is remained complete unclear because I don't know what the syntax:

$$\lambda x . x (\lambda y .y)$$

means. Can someone clarify to me how to proof this rigurously using alpha-conversion et al?

i.e. without using $$\beta$$ equivalence which is the application rule I assume.

The two terms are in the same $$\alpha$$-equivalence class. In lamba calculus, we can rename bound symbols without changing the meaning of the term. $$\lambda x.x$$ and $$\lambda y.y$$ both mean "a function that takes one input and returns it". A variable is bound by the first matching lambda above it in the term-tree.
We often $$\alpha$$-rename bound variables before $$\beta$$-reduction to make sure unbound variables do not get caputured after the reduction step.
$$\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda x.x (\lambda x'.x')$$ (rename bound $$y$$)
$$\equiv_{\alpha} \lambda y.y (\lambda x'.x')$$ (rename bound $$x$$) $$\equiv_{\alpha} \lambda y.y (\lambda x.x)$$ (rename bound $$x'$$)
This gives us $$\lambda x . x (\lambda y .y) \equiv_{\alpha} \lambda y.y (\lambda x.x)$$