(NB: λ-calculus n00b here!)

I derive the following: $$ \lambda x.\lambda y.xy \equiv \lambda x.(\lambda y.xy) \equiv \lambda x.x $$

To check myself, I tried to reduce the same expression with several online "λ-calculus calculators" (e.g. the λ Calculus Calculator or Lambda Calculator), and, to my surprise, they all agree that the original expression was already in normal form (and therefore, no further reductions are possible).

Where does my derivation go wrong?

My derivation consists of two "moves": (1) "insertion of parentheses" (just to make the evaluation order explicit), and (2) one reduction, namely $\lambda y.xy \equiv x$. The latter is an instance of what the book I am following¹ calls an "η-reduction." I figure that one of these two moves must be wrong, but I can't see how.

(FWIW, I do agree with these online calculators that the similar-looking expression $\lambda x.\lambda y.yx$ is in normal form.)

^{1 Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory (1977) by Joseph E. Stoy.}

(NB: λ-calculus n00b here!)

I derive the following: $$ \lambda x.\lambda y.xy \equiv \lambda x.(\lambda y.xy) \equiv \lambda x.x $$

To check myself, I tried to reduce the same expression with several online "λ-calculus calculators" (e.g. the λ Calculus Calculator or Lambda Calculator), and, to my surprise, they all agree that the original expression ($\lambda x.\lambda y.xy$) is already in normal form (and therefore, no further reductions are possible).

Where does my derivation go wrong?

My derivation consists of two "moves": (1) "insertion of parentheses" (just to make the evaluation order explicit), and (2) one reduction, namely $\lambda y.xy \equiv x$. The latter is an instance of what the book I am following¹ calls an "η-reduction." I figure that one of these two moves must be wrong, but I can't see how.

(FWIW, I do agree with these online calculators that the similar-looking expression $\lambda x.\lambda y.yx$ is in normal form.)

^{1 Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory (1977) by Joseph E. Stoy.}