I need a little help with a lambda calculus reduction to normal form: $$(\lambda xxxx.xx)(\lambda x.xx)(\lambda x.x)y((\lambda x.x)x)$$ It should be solved like this: $$xx(\lambda x.x)y((\lambda x.x)x)$$ and then: $$xx(\lambda x.x)y(x)$$
This is the result of any of the lambda calculators that you can find online.
My question is: why can't I go on with reductions and make also $(\lambda x.x)y$ so the resulting expression would be $xxy(x)$?
Can you give me a complete answer, with theory of lambda calculus rules/proofs?
I really want to understand this exercise, any help would be appreciated.