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

\begin{problem}
Ackermann's function, $A: \nats \cross \nats \to \nats$, satisfies
the following equations (simplified from Tutorial 2):
\begin{align}
A(m,n) &=  2n, &&\text{if $m=0$ or $n \le 1$},\label{Am0}\\ 
A(m,n) &=  A(m-1,A(m,n-1)), &&\text{if $m > 0$ and $n > 1$}.\label{AA}
\end{align}

These equations uniquely determine Ackermann's function.  That is,
\begin{lemma*}
If $B: \nats \cross \nats \to \nats$ also satisfies
the same equations as $A$, namely,
\begin{align}
B(m,n) &=  2n, &&\text{if $m=0$ or $n \le 1$},\label{Bm0}\\ 
B(m,n) &=  B(m-1,B(m,n-1)), &&\text{if $m > 0$ and $n > 1$},\label{BB}
\end{align}
then $A = B$.
\end{lemma*}

In this question, we ask you to fill in or justify various parts of a
proof of this Lemma.   The possible justifications are listed below.
You must choose your answers from this list.

\begin{itemize}
\item one or more of the equations (\emph{indicate exactly which ones}) numbered
(\ref{Am0}), (\ref{AA}), \dots (\ref{AB})
\item $P(0)$
\item $P(m)$
\item $P(m+1)$
\item $Q_m(0)$
\item $Q_m(n)$
\item $Q_0(n)$
\item $Q_m(n+1)$
\end{itemize}

\begin{proof}
We must prove that
\begin{equation}
\forall m \forall n\; A(m,n) = B(m,n). \label{a=b}
\end{equation}

The proof is by induction on $m$.  More precisely, the main induction
hypothesis, $P(m)$, is
\[
P(m) \eqdef\ \forall n\; A(m,n) = B(m,n).
\]

\textbf{Base case}: $m=0$.  It follows directly from equation(s)
\brule{4em} \solution{\pts{1} (\ref{Am0}), ~(\ref{Bm0})}

that $A(m,n) = B(m,n)$ for all $n$, confirming that \brule{4em}
\solution{\pts{2} $P(0)$}\\
is true.

\newpage

\textbf{Induction step}: Suppose $P(m)$ holds for some fixed $m \geq
0$.  We must prove that $P(m+1)$ also holds.

Namely, assuming $\forall n\; A(m,n)=B(m,n)$, we must prove
(\textbf{fill-in}):
\begin{equation}
\forall n\; \brule{2in} \text{\solution{\pts{3} $A(m+1,n)=B(m+1,n)$}} \label{m+1}
\end{equation}

We prove~(\ref{m+1}) by another induction, this time on $n$,
using the induction hypothesis,
\[
Q_m(n) \eqdef\ A(m+1, n) = B(m+1,n).
\]

%%\begin{quotation}
\addtolength{\leftskip}{0.5in}%

\textbf{Base case}: $n=0$.  $Q_m(0)$ follows immediately from equation(s)
\brule{4em}.  \solution{\pts{2} (\ref{Am0}), ~(\ref{Bm0})}

\textbf{Induction step}: Suppose $Q_m(n)$ holds for some $n \geq 0$.  We
must prove that $Q_m(n+1)$ also holds.

Let $k \eqdef A(m+1, n)$, so
\begin{equation}
A(m+1, n+1) = A(m,k)\label{Ak}
\end{equation}
by \brule{1in} \solution{\pts{3} (\ref{AA})}.

Then also
\begin{equation}
k = B(m+1, n),\label{kB}
\end{equation}
because \brule{1in} \solution{\pts{4} $Q_m(n)$}\\
holds, and so
\begin{equation}
B(m+1, n+1) = B(m,k)\label{Bk}
\end{equation}
by \brule{1in} \solution{\pts{2} (\ref{BB})}.

But
\begin{equation}
A(m,k) = B(m,k),\label{AB}
\end{equation}
since \brule{1in}\solution{\pts{5} $P(m)$}\\
holds.  Now combining equations \brule{5em}
\solution{\pts{5} (\ref{Ak}), (\ref{Bk}), and~(\ref{AB})},\\
we obtain
\[
A(m+1, n+1) = B(m+1,n+1).
\]
That is, $Q_m(n+1)$ holds.

This completes the proof by induction on $n$ that~(\ref{m+1}) holds.
%%\end{quotation}
\addtolength{\leftskip}{-0.5in}%

So we have also completed the proof by induction on $m$ that $\forall m\;
\brule{3em}$. \solution{\pts{3} $P(m)$}\\

That is, we have proved~(\ref{a=b}), as required.

\end{proof}


\end{problem}
