Lambda the Ultimate

Hi
I tried to make reductions for usual lambda-terms "as for DeBrujn's terms". May be, it will be interesting for somebody
\begin{align*}
&(\lambda xy.x)\,y && \\
&\to [y/x]\circ\lambda y.x && (Beta)\\
&\to \lambda y.\Uparrow\![y/x]_y\circ x && (Lambda)\\
&\to \lambda y.W_y\circ[y/x]\circ x && (LiftShift')\\
&\to \lambda y.W_y\circ y && (Var)\\
&\to \lambda z.\{zy\}\circ W_y\circ y && (\alpha)\\
&\to \lambda z.W_z\circ y && (IdShift)\\
&\to \lambda z.y && (W)
\end{align*}
The line \alpha is "explicit renaming of bound variable". Details are here
http://arxiv.org/abs/1303.5039
The text isn't easy.