        \problemdata       % Takes 5 *mandatory* arguments
        {ackerman}             % latex-friendly label for the prob.
        {induction}  % The topic(s) of the problem content.
        {}               % Source (if known)
        {F01 tut2-4} % Usage (list ones you are aware of).
        {}        % Last revision info (author, date).

\begin{problem}
Prove that Ackerman's function (as specified in Rosen before
Exercise 3.3.36) is a uniquely defined total function on $\nats \cross
\nats$. Definition of Ackerman's function:
$$ 
A(m,n)=
\begin{cases}
2n &\text{if $m=0$}\\ 
0 &\text{if $m \geq 1$ and $n=0$}\\
2  &\text{if $m \geq 1$ and $n=1$}\\
A(m-1,A(m,n-1)) &\text{if $m \geq 1$ and $n \geq 2$}
\end{cases}.
$$

\solution{
We have to prove that:
\begin{enumerate}

    \item \label{unique} There is a unique proposed definition for all
    pairs $(m,n) \in \mathbb{N} \times \mathbb{N}$.

    \item \label{consis} The proposed definition is consistent (in
    particular there is no circular reference).
\end{enumerate}

\begin{proof}
\ref{unique}:
Let $\left\{
\begin{array}{l}
\mathcal{E}_1 = \{ (m,n) \in \mathbb{N} \times \mathbb{N} \, | \, m = 0 \} \\
\mathcal{E}_2 = \{ (m,n) \in \mathbb{N} \times \mathbb{N} \, | \, m \geq 1$ and $n = 0 \} \\
\mathcal{E}_3 = \{ (m,n) \in \mathbb{N} \times \mathbb{N} \, | \, m \geq 1$ and $n = 1 \} \\
\mathcal{E}_4 = \{ (m,n) \in \mathbb{N} \times \mathbb{N} \, | \, m \geq 1$ and $n \geq 2 \} \\
\end{array}
\right.$

It is easy to see that the four sets above form a partition of $\mathbb{N}
\times \mathbb{N}$.

As there is a unique definition in each of these cases, overall, there is
a unique proposed definition for all pairs $(m,n) \in \mathbb{N} \times
\mathbb{N}$.

\end{proof}

\begin{proof}
\ref{consis} 

The proof uses a double induction, first on $m$, then on $n$.

More precisely, let us prove by induction on $m$ that:\\
$\forall m \in \mathbb{N}, \, \mathcal{P}(m): \; A(m,n)$ is properly defined for all $n \in \mathbb{N}$, and is a natural number.
\begin{itemize}
    \item Basis: $m=0$.\\
        This is the first case in the proposed definition.
        Since $2n$ is a natural number for all $n \in \mathbb{N}$, $\mathcal{P}(0)$ trivially holds.
    \item Inductive step: suppose $\mathcal{P}(m-1)$ holds for some $m \geq 1$,
        and let us prove that $\mathcal{P}(m)$ also holds.\\
        What we need to prove is that:\\
        $\forall n \in \mathbb{N}, \mathcal{Q}(n): \; A(m,n)$ is properly defined, and is a natural number.\\
        We will prove this assertion by induction on $n$.
    \begin{itemize}
        \item Special case: $n'=0$.\\
            This is the second case in the proposed definition.
            Since $0$ is a natural number, $A(m,0)$ is properly defined.
        \item Basis: $n'=1$.
            (We do not use the case $n'=0$ as the basis, since the recursive definition holds for $n' \geq 2$).\\
            This is the third case in the proposed definition.
            Since $2$ is a natural number, $A(m,1)$ is properly defined.
        \item Inductive step: suppose $\mathcal{Q}(n'-1)$ holds for some $n' \geq 2$,
            and let us prove that $\mathcal{Q}(n')$ also holds.\\
            $\mathcal{Q}(n'-1)$ means that $A(m,n'-1)$ is properly defined and is a natural number.\\
            Then we can use $\mathcal{P}(m-1)$ for the particular value $n=A(m,n'-1)$, which yields that
            $A(m,n')=A(m,A(m,n'-1))$ is properly defined and is a natural number.\\
            This is exactly $\mathcal{Q}(n')$.
    \end{itemize}
\end{itemize}

\end{proof}

\subsection{Remarks:}

In our induction hypothesis, we included, along with the required property
that $A(m,n)$ is properly defined, the additiona property that it's value
is a natural number.  Though this additional property was not what had
been asked to prove, we needed it for our proof.  This is another example
of the phenomenon discussed in lecture: using induction, it can be easier
to prove ``harder'' theorem than the one first given original.
}
\end{problem}
