= Solution
We use <rooted-tree homeomorphic embedding>: an injective <vertex> map preserves ancestors and lowest common ancestors, while an <edge> may map to a longer path. The root may map below the host root. Write $T\preceq U$ for this relation. The assertion of <Kruskal's tree theorem> is that finite <rooted trees> form a <well-quasi-ordering>: every infinite <sequence> has $i<j$ with $T_i\preceq T_j$.
We first supply the <word> lemma needed in the proof. In a <well-quasi-order> $Q$, every <sequence> has an infinite nondecreasing <subsequence>. Indeed, if no term had infinitely many later terms above it, successive choices beyond the finite <sets> of later dominators would give a <bad sequence>. Some term therefore has infinitely many later dominators; repeat the argument inside that infinite <subsequence>, which is still well-quasi-ordered, to build a chain.
Now order finite <words> over $Q$ by <subsequence> embedding with coordinatewise increase. Suppose a bad <word> <sequence> exists and choose one $w_0,w_1,\ldots$ minimally: at each position use a <word> of least length allowing a bad continuation of the fixed prefix. No <word> is empty. Write $w_i=v_i a_i$, removing its last letter. Choose indices $i_0<i_1<\cdots$ with $a_{i_0}\le a_{i_1}\le\cdots$. The <sequence>
$$
w_0,\ldots,w_{i_0-1},v_{i_0},v_{i_1},\ldots
$$
would also be bad. An old <word> embedding into $v_{i_j}$ embeds into $w_{i_j}$, contrary to the original badness; and $v_{i_j}\preceq v_{i_l}$ would extend, using the last-letter comparison, to $w_{i_j}\preceq w_{i_l}$. But $v_{i_0}$ is shorter than $w_{i_0}$, contradicting minimality. This proves <Higman lemma>, including its empty-word case.
Suppose next that there is a <bad sequence> of finite <rooted trees>, and choose a <minimal bad sequence> $T_0,T_1,\ldots$ by <vertex> count. Let $\mathcal S$ consist of all proper rooted subtrees hanging below <vertices> of the $T_i$. This collection is well-quasi-ordered. Otherwise choose a <bad sequence> $S_0,S_1,\ldots$ in $\mathcal S$. Its containing-tree indices can be selected strictly increasing, say $S_j$ is a proper subtree of $T_{i_j}$: a finite initial collection of containing <trees> has only finitely many proper subtrees, and a <bad sequence> cannot repeat an <isomorphism> class. Then
$$
T_0,\ldots,T_{i_0-1},S_0,S_1,\ldots
$$
is bad. No earlier $T_l$ can embed into $S_j$, because $S_j\preceq T_{i_j}$ and this would contradict the original <sequence>. The new tail is bad by construction. Since $|S_0|<|T_{i_0}|$, this contradicts minimality.
List each <tree>'s immediate root subtrees in any chosen order. These are finite <words> in the <well-quasi-order> $\mathcal S$, so the <word> lemma gives $i<j$ for which the child <word> of $T_i$ embeds into that of $T_j$. Send the root of $T_i$ to the root of $T_j$, and use the chosen embeddings inside the selected, distinct target branches. The connecting paths from the target root to the images of the source children have disjoint interiors; lowest common ancestors in different branches are preserved. This constructs $T_i\preceq T_j$, the final contradiction. Thus \b[finite <rooted trees> are well-quasi-ordered by homeomorphic embedding]. If labels lie in an arbitrary <well-quasi-order>, the same proof uses label-monotone embeddings; compare root labels and child <words> in their product <well-quasi-order>. The product property follows by taking a nondecreasing <subsequence> in the first coordinate and a good pair in the second.
For <Friedman's finite form of Kruskal's theorem>, fix $k$. Consider all finite bad prefixes $(T_1,\ldots,T_l)$ satisfying $|T_i|\le k+i$, up to rooted-tree <isomorphism>. They form a prefix <tree>. At each node there are finitely many possible next <trees>, because there are only finitely many rooted-tree <isomorphism> types on at most $k+l+1$ <vertices>. If prefixes of arbitrary length existed, the <König infinity lemma> would give an infinite branch, hence an infinite <bad sequence>, contrary to what we proved. Its height is therefore bounded. Consequently
$$
\boxed{\forall k\ \exists N\ \forall(T_1,\ldots,T_N),\quad |T_i|\le k+i\ \Longrightarrow\ \exists i<j\ (T_i\preceq T_j).}
$$
The same finite-prefix argument works with a fixed finite label alphabet, and more generally with any prescribed size bound $b(i)$ having only finitely many possibilities at each position. These are finite existence statements; no numerical estimate on $N$ is needed for the conclusion.
Back to article page
