Good examples of double induction I'm looking for good examples where double induction is necessary. What I mean by double induction is induction on $\omega^2$. These are intended as examples in an "Automatas and Formal Languages" course.
One standard example is the following: in order to cut an $n\times m$ chocolate bar into its constituents, we need $nm-1$ cuts. However, there is a much better proof without using induction.
Another example: the upper bound $\binom{a+b}{a}$ on Ramsey numbers. The problem with this example is that it can be recast as induction on $a+b$, while I want something which is inherently inducting on $\omega^2$.
Lukewarm example: Ackermann's function, which seems to be pulled out of the hat (unless we know about the primitive recursive hierarchy).
Better examples: the proof of other theorems in Ramsey theory (e.g. Van der Waerden or Hales-Jewett). While these can possibly be recast as induction on $\omega$, it's less obvious, and so intuitively we really think of these proofs as double induction.
Another example: cut elimination in the sequent calculus. In this case induction on $\omega^2$ might actually be necessary (although I'm not sure about that).
The problem with my positive examples is that they are all quite technical and complicated. So I'm looking for a simple, non-contrived example where induction on $\omega^2$ cannot be easily replaced with regular induction (or with an altogether simpler argument). Any suggestions?
 A: Though you've already dismissed it as 'lukewarm', Ackermann's function (proving totality I think is what is wanted) is your most accessible option (I think it is a great option). 
It's not contrived/unnatural because it is motivated by very different concepts. If you want to construct another example (prove $f(x,y) = g(x,y)$), you'd probably want to have x and y very much asymmetric (in the sense that they should be used in syntactically very different ways in the computations). And Ackermann's function does just that.
A: One could concoct a simple example, like proving that every sequence of the following moves on pairs of natural numbers eventually terminates:
$(i,j)\mapsto (i-1,N)$ for any natural number $N$.
$(i,j)\mapsto (i,j-1)$
(Edited to make it an inherently $\omega^2$ problem.)
A: What about prove $m+n = n+m$ for $m,n \in \mathbb{N}$? In particular, see this (site talking about double induction).
A: Let [n] denote the ordered set (0, ..., n). Show that there are precisely $\binom{n+m+1}{n+1}$ order-preserving maps $[n] \rightarrow [m]$. Also note that the collection of objects [n], together with order-preserving functions, forms a category... one can show by double induction that every map has an epi-monic factorization. I haven't actually tried doing these without double induction... it just seemed more natural that way, so I don't really know whether this is a good example, or I was just being silly. 
A: I suggest the following proof for Bezout's identity. It is a double induction, in a sense, since it proves a proposition for all pairs $a,b$ of natural numbers, by using "regular" induction on $\min(a,b)$. (I propose this as a general way to prove a statement on multiple natural variables: choose a function $f(n_1,\ldots,n_k)\mapsto N$ and then show that for all $n$, if $f(n_1,\ldots,n_k)= n$ then $n_1,\ldots,n_k$ satisfy the statement. This is then proved by induction on $n$).
Theorem: Let $a$ and $b$ be natural numbers and let $d = GCD(a,b)$ be their greatest common divisor. Then there exist integer $x$ and $y$ such that $d = ax +by$.
Proof: We use induction on $b=\min\{a, b\}$. Base case: If  $b=1$ then $d=1$, and, for $x=0$, $y=1$ it is $1= ax + by$. Inductive step: Assume that for each pair $a,b$, with $a\ge b$ and $b\in \{1, 2,\ldots, n-1\}$ there are integers $x,y$ such that $GCD(a,b) = ax + by$. Consider a pair $a,b$ with $a\ge b$ and $b=n$, and let $q$ and $r$ be the quotient and remainder in the division of $a$ by $b$. If $r=0$ then $GCD(a,b)=b = ax +by$ for $x=0$ and $y=1$.
Otherwise, being $d= GCD(a,b) = GCD(b,r)$, from the inductive hypothesis there are integers $x'$, $y'$ such that
$d=bx' + ry'$. By replacing $r=a-qb$ we get  $d=bx' +(a-qb)y' = ay' +b(x'-qy') = ax + by$ for $x=y'$ e $y=x'-qy'$.
\QED
Giuseppe Lancia (giulan@gmail.com)
A: A nice example arises by relativizing Goodstein's Theorem from $\rm\ \epsilon_0 = \omega^{\omega^{\omega^{\cdot^{\cdot^{\cdot}}}}}$ down to $\rm\ \omega^2\:.\ $
$\rm\ \omega^2\ $ Goodstein's Theorem $\  $  Given naturals $\rm\ a,\:b,\:c\ $ and an arbitrary increasing "base-bumping" function $\rm\ g(n)\ $ on $\:\mathbb N\:$ the following iteration eventually reaches $0\ $ (i.e. $\rm\ a = c = 0\:$).
$\rm\quad\quad\quad\quad\ \ a\ b + c \ \ \to\quad\quad\ \ a\ \ \ \ \ g(b)\ +\ \ \ c\ \ -\ 1\quad if\quad\ c > 0 $
$\rm\quad\quad\quad\quad\ \ \phantom{a\ b + c}\ \ \to\ \   (a-1)\ g(b)\  +\  g(b)-1\quad if\quad \ c = 0 $
Note: $\ $  The above iteration is really on triples $\rm\ (a,b,c)\ $ but  I chose the above notation in order to emphasize the relationship with radix notation and with Cantor Normal form for ordinals < $\epsilon_0$. $\ \ $ For more on Goodstein's Theorem see the link in Andres's post or see my 1995\12\11 sci.math post.
A: Let me begin with an example of an induction of length $\epsilon_0$: The proof that Goodstein sequences terminate. I mention this because when I decided to understand this result, I began to compute the length of these sequences and eventually came to a conjecture for a general formula (!) for the length of the sequence. It turned out that proving the conjecture was easy, because the proof organized itself as an induction of length $\epsilon_0$. I was both very amused and very intrigued by this. The little paper that came out of this adventure is here. 
Now, I also found once a natural example of an induction of length $\omega^2$ when studying a "Ramsey type" problem: the size of min-homogeneous sets for regressive functions on pairs. What I liked about this example is that Ackermann's function injected itself into the picture and ended up providing me with the right rates of growth. The details are in a paper here.
A: There is a double induction in the recent paper David G Glynn, "A condition for arcs and MDS codes", Des. Codes Cryptogr. (2011) 58:215-218.  See Lemma 2.4.  It is about an identity involving subdeterminants of a general matrix and appears to need a double induction.
A: For equations of parabolic or hyperbolic type in two independent variables the integration process is essentially a double induction. To find the values of the dependent variables at time t + Δt one integrates with respect to x from one boundary to the other by utilizing the data at time t as if they were coefficients which contribute to defining the problem of this integration.
