= Solution
For finite <rooted trees>, use <rooted-tree homeomorphic embedding>: an <injective> vertex map preserves ancestors and <lowest common ancestors>, so edges may become paths and distinct branches remain distinct. The root can map to a vertex below the host root. More generally label vertices in a <well-quasi-ordering> $Q$ and require each source label to precede its image label. We prove this stronger <labelled version of Kruskal's tree theorem>, from which the unlabelled result follows by taking one label.
We first need the finite-word closure, and prove it rather than merely invoking <Higman lemma>. If finite <words> over $Q$ were not a <well-quasi-ordering> under order-preserving <subsequence> embedding with increased labels, choose a <minimal bad sequence> $w_0,w_1,\ldots$, minimizing the length of $w_n$ among <words> admitting a bad continuation of the already chosen prefix. No $w_n$ is empty. Write $w_n=v_na_n$ by removing its last letter. The <perfect subsequence lemma> gives $n_0<n_1<\cdots$ with $a_{n_r}\le a_{n_s}$ for $r<s$.
The <sequence> $w_0,\ldots,w_{n_0-1},v_{n_0},v_{n_1},\ldots$ is still bad. An earlier $w_i$ embedding into a later $v_{n_r}$ would embed into $w_{n_r}$, contradicting the original <sequence>. An embedding of $v_{n_r}$ into $v_{n_s}$ extends by the last-letter comparison to an embedding of $w_{n_r}$ into $w_{n_s}$. Both possibilities are excluded. This contradicts minimality at position $n_0$, since $v_{n_0}$ is shorter. Thus the finite-word closure holds. The <perfect subsequence lemma> also proves finite product closure: first pass to a nondecreasing <subsequence> in one coordinate, then in the next, preserving all previous comparisons.
Suppose now that the labelled trees admit a <bad sequence> $T_0,T_1,\ldots$. Choose a <minimal bad sequence> by vertex number. Let $\mathcal U$ be all the proper descendant-rooted subtrees of these trees. We claim that $\mathcal U$ is a <well-quasi-ordering>. If it had a <bad sequence> of subtrees $U_r$, its parent indices can be made strictly increasing, say $U_r$ comes from $T_{n_r}$. Indeed each finite initial collection of parent trees has only finitely many subtrees, and a <bad sequence> cannot contain infinitely many terms from a finite collection. Passing to a <subsequence> therefore makes $n_0<n_1<\cdots$.
Then $T_0,\ldots,T_{n_0-1},U_0,U_1,\ldots$ is bad. A prefix tree embedding into $U_r$ would embed into its parent $T_{n_r}$, contrary to the original badness, and the tail is bad by construction. But $U_0$ has fewer vertices than $T_{n_0}$, contradicting minimality. This proves the claim.
Give the children of each root any fixed order. Its forest of child subtrees is a finite <word> in $\mathcal U$. The <word> theorem and finite product closure show that the pairs consisting of the root label and the child-subtree <word> are a <well-quasi-ordering>. Thus some $i<j$ have comparable root labels and an embedding of the child <word> of $T_i$ into that of $T_j$. Map the source root to the target root and use the obtained embeddings inside distinct target child subtrees. The paths from the target root into those distinct branches are disjoint except at the root, so this is a <label-monotone tree embedding>. It contradicts badness. Hence
$$
\boxed{\text{finite rooted trees labelled in a WQO are a WQO under homeomorphic embedding.}}
$$
For <Friedman's finite form of Kruskal's theorem>, fix $k\in\mathbb N$. \b[There is $N(k)$ such that any $N(k)$ trees with $|T_i|\le k+i$ contain $i<j$ with $T_i\preceq T_j$.] Use indices starting at zero; shifting them only changes $k$. To prove this uniform finite bound, form the <finite bad-sequence tree> of finite bad prefixes obeying the size bounds. At position $i$ there are only finitely many rooted-tree <isomorphism> types with at most $k+i$ vertices, so every node has finitely many successors.
If no bound existed, this tree would have nodes of arbitrarily large depth. A node with arbitrarily long extensions has a child with arbitrarily long extensions, since it has only finitely many children. Choosing such a child repeatedly produces an infinite branch, as in the <König infinity lemma>. The branch is an infinite bad tree <sequence>, contradicting the theorem just proved. Therefore the required $N(k)$ exists. The same proof works with any fixed finite label alphabet and any specified size bound finite at each position.
Back to article page
