Ackermann function $A(x,y)$: Prove that $A(4,y) = \underbrace{2^{2^{.^{\cdot^2}}}}_\textrm{y+3 times} -3$. Prove that $A(4,y) = \underbrace{2^{2^{.^{\cdot^2}}}}_\textrm{y+3 times} -3$.
I'm having trouble with proving that there are indeed $y+3$ exponentiations:
\begin{align*}
A(4,y) &= A(3, A(4,y-1))\\
&= 2^{A(4,y-1)+3}-3\\
&= 2^{2^{A(4,y-2)}-3+3}-3\\
&= 2^{2^{A(4,y-2)}}-3\\
&= 2^{2^{.^{.^{2^{A(4,0)}}}}}-3
\end{align*}
So far, according to my understanding, we have $y$ exponentiations. Now by considering that $A(4,0) = A(3,1) = 2^4-3 = 2^{2^2}-3$, we get additionally $2$ exponentiations for a a total of $b+2$.
Where is the missing exponent?

Prove by induction that
$$A(1,n)=n+2$$
Use this to prove by induction that
$$A(2,n)=2(n+3)-3$$
Use this to prove by induction that
$$A(3,n)=2^{n+3}-3$$
And use this to prove by induction that
$$A(4,n)=^{n+3}2-3$$
where we used tetration notation.
$$\begin{align}A(4,n+1)&=A(3,A(4,n))\\&=2^{(^{n+3}2-3)+3}-3\\&=2^{(^{n+3}2)}-3\\&=^{n+4}2-3\end{align}$$
Thus, it holds by induction.

As a bonus, see if you can prove by induction that
$$A(k,n)=2\uparrow^{k-2}(n+3)-3$$
where we use Knuth's up-arrow notation.
