I came across the definition of beta reduction in Lambda Calculus which is : $$(λx.M)N \rightarrow_β Μ[\space x:= N \space]$$ under the constraint that the $FV(N)$ are still free after the substitution.
I also came across three examples and the third one confuses me :
1st example : $$(λx.zx)w \rightarrow_β zw $$
2nd example : $$(λy.zy(λx.xy))w \rightarrow_β zw(λx.xw) $$
3rd example : $$λz.(λf .λx. f z x) (λy.y) \\ \rightarrow_β \\ λz.λx.(λy.y) z x \\ \rightarrow_β \\ λz.λx.z x \\$$
At first I thought that the left most bound variable gets substituted but in the 3rd example this does not seem to be the case.
Then I thought that given the fact that $N = (λy.y)$ is an abstraction maybe the $λf$ notation implies that it's argument will be an abstraction and so the bound variable $z$ will be "skipped".
Is my process here right and if that's the case why does the bound $z$ variable gets "skipped"? $z$ could be a notation for an abstraction as well.
Edit : Changed the word function to abstraction because as far as I understand everything can be represented via a function in $λ$-calculus.