= Solution
Use the <rooted-tree homeomorphic embedding> relation: an injective map of vertices preserves <lowest common ancestors>, so edges may become paths and the source root may map below the target root. We prove the stronger labelled statement for labels in any <well-quasi-ordering> $Q$, with labels increasing under the embedding. Forgetting labels gives <Kruskal's tree theorem>.
First every infinite <sequence> in a <well-quasi-ordering> has an infinite nondecreasing <subsequence>. Colour its index pairs according as the earlier term is or is not below the later term. <Ramsey's theorem> gives an infinite constant-colour <subsequence>; the bad colour would contradict <well-quasi-ordering>. Applying this successively in each coordinate proves <finite product closure of well-quasi-orderings>.
We need <Higman lemma> with its proof. Order finite <words> over $Q$ by <subsequence> embedding with increased letters. If there were a <bad sequence>, choose one $w_0,w_1,\ldots$ minimally: at each position choose a shortest word admitting a bad continuation of the fixed prefix. No word is empty. Write $w_n=u_na_n$, separating the last letter, and choose $n_0<n_1<\cdots$ with $a_{n_0}\leq a_{n_1}\leq\cdots$. Consider
$$
w_0,\ldots,w_{n_0-1},u_{n_0},u_{n_1},\ldots.
$$
An earlier prefix word cannot embed in a later $u_{n_j}$, since it would then embed in $w_{n_j}$. Nor can $u_{n_i}$ embed in $u_{n_j}$: adding the comparable last letters would embed $w_{n_i}$ in $w_{n_j}$. Thus the displayed <sequence> is bad, contradicting minimality at $n_0$, since $u_{n_0}$ is shorter. \b[Finite words over a well-quasi-order are <well-quasi-ordered>.]
Now suppose labelled <rooted trees> admit a bad <sequence> $T_0,T_1,\ldots$, chosen minimally in vertex count at each position. Let $\mathcal A$ consist of all proper rooted subtrees of these trees, rooted at a descendant and containing all its descendants. We claim $\mathcal A$ is <well-quasi-ordered>. Otherwise take a bad <sequence> $S_0,S_1,\ldots$ from $\mathcal A$. Only finitely many subtrees come from any fixed finite prefix of the $T_n$'s, and a bad <sequence> cannot repeat an object. Thin it so that $S_i$ comes from $T_{m_i}$ with $m_0<m_1<\cdots$. The <sequence>
$$
T_0,\ldots,T_{m_0-1},S_0,S_1,\ldots
$$
is bad: $T_j\preceq S_i$ would imply $T_j\preceq T_{m_i}$, since a rooted subtree embeds in its host; comparisons within the $S_i$'s are excluded by their <choice>. But $S_0$ is strictly smaller than $T_{m_0}$, contradicting minimality. This proves the claim.
Choose an arbitrary ordering of the children of each $T_n$. Record its root label and the finite word of rooted child-subtrees:
$$
\left(\ell_n,\ (T_{n,1},\ldots,T_{n,r_n})\right)\in Q\times\mathcal A^*.
$$
By <Higman lemma> and finite product closure, two records, with indices $i<j$, are comparable. Map the root of $T_i$ to the root of $T_j$, and map its selected child-subtrees into the distinct selected branches of $T_j$. Within a branch the embeddings preserve lowest common ancestors; between different branches both lowest common ancestors are the roots. Labels increase everywhere. This gives $T_i\preceq_Q T_j$, contradicting badness. \b[Finite labelled <rooted trees> are <well-quasi-ordered> by label-monotone homeomorphic embedding.] In particular, this proves the unlabelled theorem. A root-preserving variant follows by giving the root a special incomparable label unavailable at nonroot vertices; the general labelled theorem then forces root to root. Adjacency-preserving embeddings are a different, more restrictive relation and do not satisfy the same assertion.
For <Friedman's finite form of Kruskal's theorem>, fix $k\in\mathbb N$ and consider finite bad <sequences> satisfying $|T_i|\leq k+i$, with indices starting at $1$. Their prefixes form a <finite bad-sequence tree>. At each depth there are only finitely many possible unlabelled tree isomorphism types below the size bound, so this tree is finitely branching. If bad <sequences> existed at every finite length, <König infinity lemma> would yield an infinite branch, hence an infinite bad <sequence> of <rooted trees>, contrary to what was just proved. Therefore
$$
\boxed{\forall k\ \exists N\ \forall(T_1,\ldots,T_N)\
\left[(\forall i\leq N)\ |T_i|\leq k+i\ \Longrightarrow\
(\exists i<j\leq N)\ T_i\preceq T_j\right].}
$$
The same proof works with any fixed finite label <set>. The finite size bounds are what make the bad-prefix tree finitely branching; the proof does not claim a small effective numerical bound.
Back to article page
