Explicit renaming of bound variables

I tried to make reductions for usual lambda-terms "as for DeBrujn's terms". May be, it will be interesting for somebody
&(\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)
The line \alpha is "explicit renaming of bound variable". Details are here
The text isn't easy.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

* I'm getting [Math Processing Error]

* And now I'm not. Sorry for the noise.