2. The main theorem

Theorem. If $P$ is well partially ordered, then so is $P ^ *$, the set of finite words (finite sequences) from $P$, where $p_1 p_2 \cdots p_k \leq q_1 q_2 \cdots q_n$ means that $p_1 \leq q_{i_1}$, $p_2 \leq q_{i_2}$, ..., $p_k \le q_{i_k}$ for some $i_1 < i_2 < \cdots < i_k$.

Note that Example (c) above is the case where $P$ is totally unordered.

Some useful notation: Let us write $p,q,\ldots$ for elements of $P$ and ${\bf s}, {\bf t}, \ldots$ for elements of $P ^ *$. The empty sequence is allowed. Let $P_{\not\geq q,\geq r}$ mean $\{ p \in P : p \not\geq q, p \geq r \}$, let $(P ^ *)_{\geq {\bf t}}$ mean $\{ {\bf s} \in P ^ * : {\bf s} \geq {\bf t}\}$, etc. Observe that $P_{\geq q}$ is an upset of $P$ and $P_{\not\geq p}$ is a downset. Also observe that for $q \in P$, $(P _ {\not\geq q}) ^ *$ is the same thing as $(P ^ *)_{\not\geq q}$ (where $q$ is regarded as a one-letter word).

Proof of the Theorem.

Suppose $P ^ *$ is not wpo. Let $D$ be a downset of $P$ minimal with respect to the property that $D ^ *$ is not wpo; by Observation 5, such a $D$ exists. Without loss of generality, $D$ is $P$. Then for all $q \in P$, $(P _ {\not\geq q}) ^ *$, or equivalently $(P ^ *)_{\not\geq q}$, is wpo. In contrast, $(P ^ *)_{\not\geq {\bf s}}$ is not wpo for some string ${\bf s} \in P ^ *$ in place of $q$; indeed, let ${\bf s}$ be any element of an infinite antichain or strictly decreasing sequence in $P ^ *$.

Re-choose ${\bf s}$ if necessary to have the least possible length. Write ${\bf s} = p_1 p_2 \cdots p_k$. Clearly ${\bf s}$ is not empty, so $k \geq 1$. Let ${\bf s}'$ be the shorter string $p_1 p_2 \cdots p_{k-1}$ (empty if $k = 1$). Then $(P ^ *)_{\not\geq {\bf s}'}$ is wpo.

Now examine $(P ^ *)_{\not\geq {\bf s},\geq {\bf s}'}$. Let ${\bf t}$ be one of its elements. Since ${\bf t} \geq {\bf s}'$, we can write ${\bf t} = {\bf t}_1 q_1 {\bf t}_2 q_2 \cdots {\bf t}_{k-1} q_{k-1} {\bf t}_k$, where $q_i \geq p_i$. In fact, by choosing ${\bf t}_1, {\bf t}_2, \ldots, {\bf t}_{k-1}$ as short as possible in turn (so that ${\bf t}_1$ stops just before the first element that is $\geq p_1$, etc.), we have ${\bf t}_i \not\geq p_i$, for all $i < k$. Since ${\bf t} \not\geq {\bf s}$, we have ${\bf t}_k \not\geq p_k$ as well. In other words, $(P ^ *)_{\not\geq {\bf s},\geq {\bf s}'}$ is an isotone image of part of $(P ^ *)_{\not\geq p_1} \times P \times (P ^ *)_{\not\geq p_2} \times P \times \cdots \times P \times (P ^ *)_{\not\geq p_k}$, so is wpo. But then $(P ^ *)_{\not\geq {\bf s}}$, which is the union of the wpo sets $(P ^ *)_{\not\geq {\bf s},\geq {\bf s}'}$ and $(P ^ *)_{\not\geq {\bf s}'}$, is also wpo, a contradiction.