Combinatory logic - Evaluation exercise (abstraction and weak reduction)

Question

I am going through the book "Lambda-Calculus and Combinators: An Introduction".

I am trying to solve the following exercise: evaluation of $[x,y,z].xzy$

The result should be, according to solutions: $\mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})(\mathbf{S}(\mathbf{K}\mathbf{K})\mathbf{S}))(\mathbf{K}\mathbf{K})$

My attempt is the following:

$[x,y,z].xzy \\ \equiv [x].([y].([z].xzy)) \\ \equiv [x].([y].\mathbf{S} x(\mathbf{K} y))\\ \equiv [x].(\mathbf{S}([y].\mathbf{S} x)([y].\mathbf{K} y)) \\ \equiv [x].(\mathbf{S}(\mathbf{K}\mathbf{S}x)\mathbf{K})\\ \equiv \mathbf{S}([x].\mathbf{S}(\mathbf{K}\mathbf{S}x))([x].\mathbf{K}) \\ \equiv \mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})([x].\mathbf{K}\mathbf{S}x))(\mathbf{K}\mathbf{K}) \\ \equiv \mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})(\mathbf{K}\mathbf{S}))(\mathbf{K}\mathbf{K}) $

but it does not match the solution.

Answer 1

$ [x,y,z].xzy \\ \equiv [x].([y].([z].xzy)) \\ \equiv [x].([y].(\mathbf{S}([z].xz)([z].y))) \\ \equiv [x].([y].(\mathbf{S}x(\mathbf{K}y))) \\ \equiv [x].(\mathbf{S}([y].\mathbf{S}x)([y].\mathbf{K}y)) \\ \equiv [x].(\mathbf{S}([y].\mathbf{S}x)\mathbf{K}) \\ \equiv [x].(\mathbf{S}(\mathbf{S}([y].\mathbf{S})([y].x))\mathbf{K}) \\ \equiv [x].\mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})(\mathbf{K}x))\mathbf{K} \\ \equiv [x].\mathbf{S}(\mathbf{K}(\mathbf{S}x))\mathbf{K} \\ \equiv \mathbf{S}([x].\mathbf{S}(\mathbf{K}(\mathbf{S}x)))([x].\mathbf{K}) \\ \equiv \mathbf{S}(\mathbf{S}([x].\mathbf{S})([x].\mathbf{K}(\mathbf{S}x)))(\mathbf{K}\mathbf{K}) \\ \equiv \mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})(\mathbf{S}([x].\mathbf{K})([x].\mathbf{S}x)))(\mathbf{K}\mathbf{K}) \\ \equiv \mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})(\mathbf{S}(\mathbf{K}\mathbf{K})\mathbf{S}))(\mathbf{K}\mathbf{K}) \\ $

This relies on the following rule (which I didn't find in the book):

$ \mathbf{S}(\mathbf{K}A)(\mathbf{K}B) \to \mathbf{K}(AB) $

Because of that, I was able to simplify as follows:

$ [x].\mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})(\mathbf{K}x))\mathbf{K} \to [x].\mathbf{S}(\mathbf{K}(\mathbf{S}x))\mathbf{K} $