Definition ($beta$-normal form). A $\lambda$-term $M$ is in $\beta$-normal form if there is no term $N$ such that $M{\to }_{\beta }N$.