Let $M \equiv \lambda z.zy$
is $M$ in $\beta$-normal form?
I know that the $\beta\text{-}nf$ class is defined as following:
(1) all atoms are in $\beta\text{-}nf$
(2) $M_1 ,...,M_n ∈ β\text{-}nf ⇒ aM_1 ...M_n ∈ β\text{-}nf\quad$ for all atoms $a$
(3) $M ∈ β\text{-}nf ⇒ λx.M ∈ β\text{-}nf$
So, by construction, I guess $M$ belongs to $β\text{-}nf$ by doing:
i) initialize a term as $y$ and call it $A_1$ (thus, $A_1 \equiv y$). By (1), $A_1 ∈ β\text{-}nf$
ii) by (2), let $n=1$ and $M_1 \equiv A_1$, so $zA_1$ should belong to $β\text{-}nf$. Let's say $A_2 \equiv zA_1$
iii) by (3), $\lambda z.A_2$ should belong to $β\text{-}nf$ since $A_2$ also does. Let's say $A_3 \equiv \lambda z.A_2$
as $A_2 \equiv zA_1$ and $A_1 \equiv y$, $A_2 \equiv zy$, thus $A_3 \equiv \lambda z.zy$
$M$ is obviously the same than $A_3$, so I guess $M$ belongs to $β\text{-}nf$. Is this right or I missed something in the way?
Indeed. There is no need to introduce the $A_\star$ symbols though.
Tokens $z$ and $y$ are atoms.
Via (1), since they are atoms, therefore $z$ and $y$, are in $\beta$-nf.
Via (2), since these atoms, $z$ and $y$, are in $\beta$-nf, therefore their product, $zy$, is too.
Via (3), since such a thing as $zy$ is in $\beta$-nf, therefore the lambda expression $\lambda z {.} zy$ is too.
Since $\bf M$ is that lambda expression, therefore $\bf M$ is in $\beta$-nf.
$\blacksquare$