Consider the untyped $\lambda$-calculus expression
$$x(\lambda y.P\;)z$$
...where (FWIW) $z$ is not free in $P$, and $P$ does not contain a redex. Can this expression be $\beta$-reduced? I've consulted several textbooks, but they are all silent on this point (as far as I can tell). Application is left-associative, so the fully-parenthesized rendition of the expression above would be
$$((x(\lambda y.P\;))z)$$
The formalism, as given in all the textbooks I've consulted, specifies a $\beta$-reduction for $((\lambda y.P\;)z)$, namely $((\lambda y.P\;)z)\; \triangleright_{\beta} \;([z/y]P\;)$, but not one for $((x(\lambda y.P\;))z)$. Therefore, the answer to my question would appear to be "no", but a derivation I'm working my way through seems to require an invalid-looking $\beta$-reduction of the form
$$((x(\lambda y.P\;))z) \;\; \triangleright_{\beta} \;\;(x([z/y]P\;))\;.$$
Any help with this would be appreciated. In particular, reference to a treatment of the $\lambda$-calculus that explicitly adjudicates this question would be very helpful. Thanks!