For computing $2+3$, the lambda calculus goes the following: $(\lambda sz.s(sz))(\lambda wyx.y(wyx))(\lambda uv.u(u(uv)))$
I am having a hard time substituing and reaching the final form of $(\lambda wyx.y((wy)x))((\lambda wyx.y((wy)x))(\lambda uv.u(u(uv))))$. Can anyone provide step-by-step procedure?
Recall that application is left-associative e.g. $w y x = \color{\red}{(}w y\color{red}{)} x$. Then the steps just follow by standard $\beta$-reduction and $\zeta_1$ (which reduces the left-hand side of an application, i.e. $e_1 \rightarrow e_1' \Rightarrow e_1 e_2 \rightarrow e_1' e_2$. In the following I have underlined the term which is about to be substituted:
$\color{red}{(}(\lambda sz.s(sz))\underline{(\lambda wyx.y(wyx))}\color{red}{)}(\lambda uv.u(u(uv)))$
$\xrightarrow{\zeta_1/\beta} (\lambda z.(λwyx.y(wyx))((\lambda wyx.y(wyx))z))\underline{(\lambda uv.u(u(uv)))}$
$\xrightarrow{\beta} (\lambda wyx.y(wyx))((\lambda wyx.y(wyx))(\lambda uv.u(u(uv))))$
Which is equal to your final form which has some additional parentheses to make clear the associativity of $w y z$ (i.e. $\lambda wyx.y((wy)x))((\lambda wyx.y((wy)x))(\lambda uv.u(u(uv))))$).