alpha equivalence of lambda calculus

I am pretty new in λ calculus. And I am now trying to understand Alpha equivalence. Basically can I think it in this way: as long as I make sure all the bound variables and their corresponding abstractions are noted as the same letter, the new expression is alpha equivalent to the old one? Here is one example:

(λx.(λx.x(λy.x)x)x)x

And by applying alpha equivalnce I can rewrite it to:

(λw.(λz.w(λy.z)z)w)x

Is my understanding correct ?

Here is one example:

(λx.(λx.x(λy.x)x)x)x

And by applying alpha equivalnce I can rewrite it to:

(λw.(λz.w(λy.z)z)w)x

Is my understanding correct ?

There is a small error in your rewriting: at λz.w you have changed the meaning of the expression, because now the bound variable refers to the outer lambda abstraction, instead of the inner lambda abstraction as before. Instead, it should be λz.z. Other than this, the rewriting is correct.

Basically can I think it in this way: as long as I make sure all the bound variables and their corresponding abstractions are noted as the same letter, the new expression is alpha equivalent to the old one?

Yes, this understanding is correct.

StackExchange Computer Science Q#128449, answer score: 3