\problemdata                                                             
        {Choose-a-tuple game} % latex-friendly label for the prob.
        {State machines} % The topic(s) of the problem content.  
        {?} % Source (if known)                                          
        {S01 Tutorial 5, 5} % Usage (list ones you are aware of). 
        {Tina Wang, S02} % Last revision info (author, date).   
                                                                         
                                                                         
\begin{problem}           
In this problem we'll generalize the choose-a-pair game to
``choose-a-tuple''.  Here are the rules:

Player 1 chooses any integer $n\geq 1$.  Then player 2 chooses any
$n$-tuple of natural numbers.  After that, the players alternate moves,
choosing at each move any $n$-tuple of natural numbers which is NOT
coordinatewise $\geq$ any previously chosen $n$-tuple.  The game ends when
some player cannot move.

For example, player 1 might begin by choosing $n=3$.  Then player 2 might
choose the 3-tuple (8, 9, 10).  Possible subsequent choices might then be
\[
(7,8,9), (0,1,67), (83, 0,0), (1,0,0), (0,0,1) (0,1,0)
\]
This finally leaves player 1 with only the move (0,0,0), and the game ends
since no more moves are possible.

It turns out that every one of these games must end at some point; no game
can go on forever!  You proved this for the $n=2$ case on Problem Set 6 by
applying an ingenious, \emph{ad hoc}, well-ordering to the states of the
game.  Rather than try to generalize that bit of ingenuity (which can get
messy), we'll help you to prove this remarkable fact by developing
properties of a special class of well-founded posets.

\begin{definition}
A poset $(P,\prec)$ is \emph{well-quasi-ordered} iff, for every nonempty
subset $S \subseteq P$ has at least one, but at most a finite number of,
minimal elements.
\end{definition}

\begin{problemparts}

\problempart Prove:
\begin{lemma}\label{coord-wqo}
Suppose  $(P, \leq_P)$ and $(Q, \leq_Q)$ are well-quasi-ordered posets.
Then so is $P \cross Q$ under the coordinatewise partial order.
\end{lemma}

\solution{

Suppose $\emptyset \neq S \subseteq P \cross Q$.  We first prove $S$ has
at least one minimal element.  This was proved in S99, Handout 18 as
follows:

\begin{proof}
Then $\set{p \in P \mid (p,q) \in S \mbox{ for some } q \in Q}$ is a
nonempty subset of $P$, and so has a $\leq_P$-minimal element $m_P$.  Now
$\set{q \in Q \mid (m_P,q) \in S}$ is a nonempty subset of $Q$ and so has
a $\leq_Q$-minimal element $m_Q$.  It follows that $(m_P,m_Q)$ is a
coordinatewise minimal element of $S$.
\end{proof}

Now suppose $S$ had an infinite set $F \subseteq S$ of minimal elements.  
Then $\set{p \in P \mid (p,q) \in F \mbox{ for some } q \in Q}$ is
a nonempty subset of $P$, and so has only finitely many minimal elements
of $P$.  TO BE COMPLETED
}

\problempart Now prove that any choose-a-tuple game must end.

\solution{
\begin{proof}
Just show by induction on $n\geq 1$ that $\naturals^n$ under
coordinatewise order is well-quasi-ordered.  The base case $n=1$ is
immediate, and Lemma~\ref{coord-wqo} handles the induction case.
\end{proof}
}

\end{problemparts}
\end{problem}                                 