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.