(^f g x. f x (g x))(^x y. x)(^x y. x)

with ^ being lambda.

The result should be ^x. x

What I have tried so far and got to a result:

-do an alfa reduction for the 2 x's at the end with z = (^z y. z)

-replace f with (^z y. z) and I get this: (^g x. ((^z y. z)) x (g x))(^z y. z)

-the I replace g with (^z y. z) and get: (^x. ((^z y. z)) x ((^z y. z) x))

-now I replace both z's with x and get: (^x. (^y. x) (^y. x))

-now since I do not have a y in the first (^y. x) I can get rid of the second (^y. x) and get finally: ^x. x

I got the right answer but I am not 100% sure it's OK how I did it. If anyone could point out if there are any errors I would appreciate it.

The second one which I can't seem to get is this:

(^y. x (^x. x))[(^y. y x)/x]

Here I am supposed to substitute x with (^y. y x). The book states that in cases like this I should rename some variables so they do not affect the expression. But I'm really confused and don't know which one. I would go for the y first because if I would substitute the first x with the expression after it that y would become bound.

If anyone could explain this example a bit that would be great.