I'm supposed to find normal form (if it exists) of following lambda term
(λy.y x (λx. y (λy.z) x)) v w
I understand first step of the process, which returns
(v x (λx.v (λy.z) x) w)
but i don't understand why this is given as final result of starting problem.
My question is: why can't i reduce that term further and have following as a result?
(v x (λx.v z) w)
Is there some specific rule that prevents me from doing that ?