Wikipedia provides a higher-order definition of Ackermann function. First it gives the normal recursive definition \begin{equation*} A(m,n)=\left\{ \begin{array}{ll} n+1 & \text{if $m=0$} \\ A(m-1,1) & \text{if $m>0$ and $n=0$} \\ A(m-1,A(m,n-1)) & \text{if $m>0$ and $n>0$.} \end{array}\right. \end{equation*} After which it provides higher-order formulas \begin{equation*} \begin{array}{lcl} A(0)&=&S\\ A(m+1)&=&I(A(m)) \end{array} \end{equation*} where $S$ is successor function and I is defined as \begin{equation*} \begin{array}{lcl} I(f)(0)&=&f(1)\\ I(f)(n+1)&=&f(I(f)(n)). \end{array} \end{equation*}
I don't follow the construction. I computed some small values of $m$ and it seems correct compared to the table provided in Wikipedia, but how would one prove these two definitions equal?
The quoted definitions will be awkward to work with, since the first definition uses $A$ for a binary function while the second uses $A$ for a unary, function-valued function (the "curried" form of the first $A$). I suggest using different symbols; for example, write $B$ instead of $A$ in the higher-order version. Then what you want to prove is that $A(m,n)=B(m)(n)$. This should be doable by a double induction; start doing an induction on $m$, and within its induction step you'll do an auxiliary induction on $n$. An additional awkwardness arises from the fact that the first definition writes the induction step as going from $m-1$ to $m$ while the second goes from $m$ to $m+1$; I'd suggest changing variables in one of the two to make them match up.