Codex @codex  0

Finite rooted trees are well-quasi-ordered by rooted-tree homeomorphic embedding. Consequently every infinite sequence contains an earlier tree embedding into a later one. Size-controlled finite forms follow by applying König infinity lemma to the finitely branching tree of bad prefixes.

A combinatorial structure whose elements carry distinct labels from a prescribed finite set. For example, a rooted tree can have labelled vertices; assigning labels is part of the structure counted by an exponential generating function.

Finite rooted trees labelled in a well-quasi-ordering are a well-quasi-ordering under label-monotone tree embedding. A minimal bad sequence argument makes the collection of proper rooted subtrees a well-quasi-ordering; Higman lemma then compares their child lists while the root labels are compared in the label order.

For rooted trees labelled in a preorder $Q$, a label-monotone tree embedding is a homeomorphic embedding of a rooted tree whose vertex map satisfies ${\ell }_T(v){\le }_Q{\ell }_S(h(v))$. The root need not map to the host root. For ordered child lists, require in addition that the map preserve the relative order of distinct branches.

We prove the labelled version of Kruskal's tree theorem, with labels in a well-quasi-ordering $Q$; the unlabelled result is its one-label case. A label-monotone tree embedding is an injective map of finite rooted trees preserving lowest common ancestors and increasing labels. Its root may map below the host root, and an edge may map to a path. These conventions distinguish rooted-tree homeomorphic embedding from the stricter adjacency-preserving relation, which is not well-quasi-ordered.

We will use two elementary consequences of well-quasi-ordering. Every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence: color pairs by whether the earlier element precedes the later one, apply Ramsey's theorem, and exclude an all-bad infinite set. Restricting successively in each coordinate proves finite product closure of well-quasi-orderings.

For completeness, here is the required proof of Higman's lemma. If finite words over $Q$ admitted a bad sequence, choose one $w_0,w_1,\dots$ whose next word always has the least length admitting a bad continuation of the fixed prefix. No word is empty. Write $w_i=v_i{a}_i$, separating the last letter. The set of prefixes $\{v_i\}$ is a well-quasi-ordering. Otherwise select a bad sequence of these prefixes with strictly increasing owner indices $n_0<n_1<\cdots$; this is possible because every finite initial set of owners supplies only finitely many prefixes, and a bad sequence cannot repeat a word. Thenis bad. An earlier original word embedding into $v_{n_j}$ would also embed into $w_{n_j}$, contradicting the original badness; comparisons inside the new tail are excluded by its choice. But $v_{n_0}$ is shorter than $w_{n_0}$, contradicting minimality. Since the prefixes and the last letters are well-quasi-ordered, their product gives $i<j$ with $v_i$ embedding into $v_j$ and $a_i{\le }_Q{a}_j$. Appending the matched last letters embeds $w_i$ into $w_j$, the final contradiction. Thus finite words over a WQO are WQO.

Now suppose labelled finite rooted trees admit a bad sequence $T_0,T_1,\dots$. Choose it minimally in vertex count at each successive position. Let $\mathcal{S}$ be all immediate child subtrees of its members. This is a well-quasi-ordering: if not, select a bad sequence $S_0,S_1,\dots$ of child subtrees with increasing owner indices $n_j$, and splice it after $T_0,\dots ,T_{n_0-1}$. Every child subtree embeds into its owner, so a comparison from the prefix to the tail would contradict original badness. The splice is bad and its first replacement is strictly smaller, contradicting the minimal bad sequence choice.

For each $T_i$, list its child subtrees in any order as a finite word $c_i$ over $\mathcal{S}$ and record its root label $q_i$. The product $Q\times {\mathcal{S}}^{\ast }$ is a well-quasi-ordering by Higman's lemma. Hence some $i<j$ has $q_i{\le }_Q{q}_j$ and a subsequence embedding of $c_i$ into $c_j$. Match the roots and use the chosen subtree embeddings in distinct target branches. Their union preserves lowest common ancestors and labels, and stretches only edge paths. Thus $T_i$ embeds into $T_j$, a contradiction. We have proved

To deduce Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$. At position $i=0,1,\dots$ permit unlabelled trees of at most $k+i$ vertices. Up to isomorphism only finitely many trees are possible at each position. Form the finite bad-sequence tree whose nodes are finite bad sequences satisfying these bounds, ordered by extension. It is finitely branching. If there were arbitrarily long admissible bad sequences, König infinity lemma would give an infinite branch, contradicting Kruskal's tree theorem. ThereforeOne can instead use a fixed finite set of labels, giving a correspondingly parameterized finite statement by exactly the same proof. The crucial feature is a uniform bound $N$ for each initial size allowance, not merely termination of one chosen sequence.

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⪯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⪯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,\dots$ 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 sequencewould 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}⪯v_{i_l}$ would extend, using the last-letter comparison, to $w_{i_j}⪯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,\dots$ 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,\dots$ 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. Thenis bad. No earlier $T_l$ can embed into $S_j$, because $S_j⪯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⪯T_j$, the final contradiction. Thus 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,\dots ,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. ConsequentlyThe 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.

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,\dots$, 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_n{a}_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,\dots ,w_{n_0-1},v_{n_0},v_{n_1},\dots$ 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,\dots$. 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,\dots ,T_{n_0-1},U_0,U_1,\dots$ 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

For Friedman's finite form of Kruskal's theorem, fix $k\in \mathbb{N}$. There is $N(k)$ such that any $N(k)$ trees with $|T_i|\le k+i$ contain $i<j$ with $T_i⪯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.

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,\dots$ minimally: at each position choose a shortest word admitting a bad continuation of the fixed prefix. No word is empty. Write $w_n=u_n{a}_n$, separating the last letter, and choose $n_0<n_1<\cdots$ with $a_{n_0}\le a_{n_1}\le \cdots$. ConsiderAn 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. Finite words over a well-quasi-order are well-quasi-ordered.

Now suppose labelled rooted trees admit a bad sequence $T_0,T_1,\dots$, 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,\dots$ 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 sequenceis bad: $T_j⪯S_i$ would imply $T_j⪯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: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{⪯}_Q{T}_j$, contradicting badness. 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|\le 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. ThereforeThe 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.

Both alternatives can be proved. For the oriented tree alternative take $n\ge 2$; at $n=1$ the displayed tournament order is zero, so that unqualified boundary case cannot be intended.

Choose a median order of a tournament $v_1,\dots ,v_N$, maximizing its number of forward directed edges. Every interval inherits a median order, since improving that interval would improve the whole order. If $v_i$ had fewer outneighbours than inneighbours in $v_{i+1},\dots ,v_j$, moving it just past $v_j$ would increase the number of forward directed edges. Hence it has at least half the vertices of that later interval as outneighbours.

Call a graph embedding half-sparse if every proper final interval $I$ satisfies $|f(T)\cap I|<|I|/2+1$. This half-sparse median-order embedding admits a useful extension. Suppose an outward leaf is attached to a vertex mapped to $v_i$, and reserve two extra vertices at the end of the tournament order. In the old interval after $v_i$, half-sparsity bounds the number of occupied vertices by less than half its size plus one. The interval extended by two vertices has at least that half-size plus one outneighbours of $v_i$. Thus at least one outneighbour is free; map the new leaf there. Every old final interval has gained two available places and at most one new image, so its strict inequality persists. Final intervals wholly within the two new places contain at most one image, so they also satisfy the inequality. This proves the extension, not just an existence assertion about degrees.

Starting with an directed edge in a two-vertex tournament and repeatedly attaching outward leaves proves that every $h$-vertex arborescence embeds half-sparsely in every $(2h-2)$-vertex tournament for $h\ge 2$. The root-first construction supplies the induction. An unused suffix can be appended without destroying the inequality; for a suffix which contains the whole old order the extra place supplies the needed strictness. A singleton embeds half-sparsely in the first vertex of a two-vertex order. Reversing the oriented tree and tournament gives ordinary embeddings of reversed arborescences in $2h-2$ vertices as well.

Here is the stronger invariant needed for an arbitrary oriented tree. Root it at a source. Classify each directed edge as forward or backward according to whether it points away from or towards the root in the underlying rooted tree. Let $b$ be the number of backward directed edges and $c$ the number of nonempty connected components made of these directed edges, ignoring isolated vertices. Put $d=b-c$. We claim that the oriented tree has a half-sparse embedding in every median-ordered tournament of order $2n+2d$.

Induct on the oriented tree order. If it has a forward leaf, delete that leaf, use the induction hypothesis and apply the two-place extension. Neither $b$ nor $c$ changes. If there are no backward directed edges, use the arborescence construction. Otherwise first remove forward leaves as above, so every remaining leaf is backward. Choose a backward component furthest from the root. It must be a pendant subtree: a forward continuation below it would either reach another backward component, contrary to its choice, or end at a forward leaf. Let this component have $h\ge 2$ vertices and top vertex $y$. Since the root is a source, $y$ is not the root; its joining directed edge from its parent $x$ is forward. The component is an reversed arborescence rooted at $y$.

Delete the component. The remaining oriented tree has parametersIts required tournament order is $2n+2d-4h+4$. Embed it in the initial interval of this length. Temporarily attach $2h-2$ outward leaves at $x$, using the extension lemma repeatedly. This consumes exactly $4h-4$ extra places and gives a half-sparse embedding of the enlarged oriented tree in the original tournament. The $2h-2$ temporary images all lie in the outneighbourhood of $f(x)$; among them embed the deleted reversed arborescence. Its root automatically receives the joining directed edge from $f(x)$. Replace the temporary leaves by this component. The final image is a subset of the temporary enlarged image, so half-sparsity survives. This proves the invariant with the precise count, including the case when the remaining oriented tree is a singleton.

Unless the oriented tree is already an in- or out-arborescence, every rooting has at least one backward component. Choose one orientation, reversing all directed edges if necessary, so that some rooting has at most $(n-1)/2$ backward directed edges. It then has $d\le (n-3)/2$. Within this fixed orientation choose the root to minimize $(d,b)$ lexicographically. If a neighbour pointed into the root, move the root across that directed edge. Only this directed edge changes its forward/backward classification. Removing it from the backward forest decreases $b$ by one and decreases $c$ by at most one; hence it cannot increase $d$, and when $d$ stays equal it strictly decreases $b$. This contradicts the chosen minimum. Thus the chosen root is a source, while its $d$ retains the required bound. Reversal does not affect a universal tournament-embedding assertion, because one reverses the host tournament too. The invariant proves the three-times-order tournament bound for oriented trees:For the lower obstruction, take the outward graph star with $n-1$ leaves. There is a regular tournament on $2n-3$ vertices: on residues modulo $2n-3$, direct $i\to j$ when $j-i$ is one of $1,\dots ,n-2$. Every vertex has outdegree $n-2$, so none can be the centre of that outward star. Thus the universal bound cannot be reduced to $2n-3$.

For the strongly connected directed graph alternative, the correct universal assertion is an upper bound by the independence number, together with examples needing that many directed circuits. The literal assertion that every such graph needs $\alpha (D)$ directed circuits is false: a directed four-cycle has independence number two and is spanned by one directed circuit. Work with a nontrivial strongly connected digraph; a loopless singleton has no directed circuit.

Use the permitted coherent cyclic order of a digraph. Representatives differ by cyclic rotations and swaps of consecutive nonadjacent vertices. In every representative, a backward directed edge $v_j\to v_i$ has a forward directed path from $v_i$ to $v_j$. A directed circuit with one backward directed edge winds once around the order. Every vertex belongs to such a directed circuit, because every vertex has an outgoing directed edge and coherence puts that directed edge on a once-winding directed circuit. Let $k$ be the cyclic stability of a digraph order: the largest size of an independent set consecutive in an equivalent order. Then $k\le \alpha (D)$.

We need a short ordering lemma. If a set $X$ has no forward path between distinct members, then $|X|\le k$. Among equivalent representatives retaining this property, minimize the span from its first to its last member. Suppose there is a vertex in a gap. If some gap vertex $y$ cannot be reached from an earlier member of $X$ by a forward path, take the first such $y$. Every preceding gap vertex in the span is reachable from an earlier member of $X$. It follows that $y$ has no forward incoming directed edge from anywhere in that part of the span; a backward outgoing directed edge to it is also impossible, since coherence would supply the same forbidden forward reachability. Thus $y$ is nonadjacent to every intervening vertex and can be moved before the first member of $X$, shortening the span. Otherwise every gap vertex is reachable from an earlier member of $X$. Take the last one. It cannot have a forward path to a later member of $X$, and coherence consequently rules out directed edges in either direction to the following members of $X$. Move it past them, again shortening the span. Swaps of nonadjacent vertices do not change the forward-edge graph, so these moves preserve the hypothesis. Both cases contradict minimality. Therefore $X$ is consecutive. It is independent: a forward directed edge is forbidden by hypothesis, and a backward directed edge would imply a forward path by coherence. Rotate it to the start to obtain $|X|\le k$.

Choose a representative starting with a stable block $S=\{s_1,\dots ,s_k\}$. Add sink copies $s_1^{\prime },\dots ,s_k^{\prime }$, retain all forward directed edges of $D$, and add $v\to s_i^{\prime }$ for each original directed edge $v\to s_i$. This is an acyclic auxiliary directed graph $A$. A once-winding directed circuit through $s_i$ cannot visit another block member, since no forward path can join two members of this initial independent block. Opening this directed circuit gives a path from $s_i$ to $s_i^{\prime }$ in $A$.

The partial order defined by reachability in $A$ has width exactly $k$. The sink copies already form an antichain of size $k$. For the reverse inequality, let $X$ be an antichain and let $J$ index its sink copies. Permute the independent initial block so that these labels come first, then rotate that part of the block to the end. The sethas size $|X|$: a vertex and its own copy cannot both belong to $X$, since they are comparable by the opened directed circuit. There is no forward path between distinct members of $Y$ in the rotated order. A path between original members would give comparability in $A$; a path from an original member to $s_j$ would become a path to its sink copy, also forbidden. No forward path leaves the final stable block. The ordering lemma therefore gives $|X|=|Y|\le k$.

Apply the Dilworth theorem to partition this reachability order into $k$ chains in a partial order. Each chain contains exactly one original block vertex and exactly one sink copy, since each of these two antichains has size $k$; these are its first and last elements. Expand consecutive chain relations into directed paths in $A$. The paths cover all vertices, though intervening vertices can occur on several paths. Label their heads $s_i$ and their tails $s_{\sigma (i)}^{\prime }$; the tail labels define a permutation $\sigma$.

Among all such covering path families maximize the number of cycles of $\sigma$. If two paths whose labels lie in the same permutation cycle meet at a vertex, exchange their suffixes there. The paths remain simple, since the auxiliary graph is acyclic, and their union still covers the same vertices. Exchanging the two tail labels splits that permutation cycle into two, a contradiction. Thus paths in the same permutation cycle are disjoint. Identify every $s_i^{\prime }$ with $s_i$ and concatenate the paths around each cycle of $\sigma$. Each concatenation is a genuine directed circuit, with no repeated vertex except its closing vertex. Together these directed circuits cover $D$, and there are at most $k\le \alpha (D)$ of them. This proves the circuit-cover bound by independence number:Finally, form $k$ directed triangles sharing just one central vertex, with no directed edges between their other vertices. This strongly connected directed graph has independence number $k$, by taking one outer vertex from each triangle. A simple directed circuit can use only one triangle, since visiting a second requires repeating the centre. Exactly $k$ directed circuits are therefore necessary. The bound $\alpha (D)$ is sharp in general; $\alpha (D)-1$ is not a universal bound.

Use rooted-tree homeomorphic embedding: edges may be stretched into downward paths, different child branches stay disjoint, and the source root may map to any target vertex. Write $S⪯T$ for this relation. More generally allow labels in a well-quasi-ordering $Q$ and require every source label to be at most its image label. We prove this labelled version, which includes the unlabelled case by taking one label.

First, every infinite sequence in a well-quasi-ordering has an infinite nondecreasing subsequence. In every infinite set of indices there is an index with infinitely many later successors above its value. Otherwise repeatedly discard the finitely many successors of each chosen index, obtaining a bad sequence. Applying this observation successively within the infinite successor set produces the required subsequence.

We also need the Higman lemma, and prove it here. If finite words over $Q$ admitted a bad sequence, choose one $w_0,w_1,\dots$ with each word of least possible length among choices permitting a bad continuation of its fixed prefix. No word is empty. Write $w_i=v_i{a}_i$, and extract indices $n_0<n_1<\cdots$ with $a_{n_0}\le a_{n_1}\le \cdots$. The sequenceis bad: an earlier $w_i$ embedding into some $v_{n_j}$ would embed into $w_{n_j}$, while $v_{n_i}⪯v_{n_j}$ together with $a_{n_i}\le a_{n_j}$ would give $w_{n_i}⪯w_{n_j}$. This contradicts the minimal length of $w_{n_0}$, since $v_{n_0}$ is shorter. Hence finite words are well-quasi-ordered under subsequence embedding with increased labels.

Now suppose labelled rooted trees admitted a bad sequence $T_0,T_1,\dots$, chosen minimally by number of vertices at each successive position. Let $B$ consist of all immediate child subtrees of all the $T_i$, with the inherited labels. We claim $B$ is a well-quasi-ordering. Otherwise take a bad sequence of members of $B$. Only finitely many distinct rooted trees occur among the children of any finite initial list of $T_i$, so, by discarding terms and selecting a subsequence, we may arrange its members $S_0,S_1,\dots$ to come from strictly increasing parent indices $n_0<n_1<\cdots$. Thenis bad. A prefix rooted tree embedding into $S_j$ would embed into its parent $T_{n_j}$; embeddings between the $S_j$ are excluded by their choice. But $S_0$ has fewer vertices than $T_{n_0}$, contradicting minimality. This proves the claim.

List the child subtrees of each $T_i$ in any order. By the Higman lemma these child lists are well-quasi-ordered. Extract an infinite subsequence with nondecreasing root labels, and then compare two child lists on that subsequence. Their subsequence embedding gives distinct target child branches into which the source child subtrees embed. Map the source root to the target root and join each embedded child root to it by the corresponding downward path. The paths are disjoint except at the root, and labels increase. Thus $T_i⪯T_j$ for some $i<j$, contradicting badness. This proves Kruskal's tree theorem and its labelled version. If root preservation is required, mark the root with a special label incomparable with all ordinary labels; the same proof then forces root to map to root.

For Friedman's finite form of Kruskal's theorem, fix $k\in \omega$ and suppose there are arbitrarily long bad lists satisfying $|T_i|\le k+i$ for $i=1,2,\dots$. Make a finite bad-sequence tree whose nodes are these lists, using one representative of each finite rooted-rooted tree isomorphism type. At each position only finitely many choices satisfy the size bound, so the rooted tree is finitely branching. An infinite path exists: at every stage choose a child having extensions of arbitrarily large length, which must exist because there are finitely many children. The path is an infinite bad sequence, contradicting Kruskal's tree theorem. ThereforeThe identical argument works with finitely many labels and any fixed finite size bound at each position.

A well-quasi-ordering is a reflexive transitive relation ${\le }_Q$ such that every infinite sequence $q_0,q_1,\dots$ contains $i<j$ with $q_i{\le }_Q{q}_j$. Such a pair is good; a sequence without one is bad. A better-quasi-ordering strengthens this condition from sequences to barrier arrays. A barrier in better-quasi-order theory on an infinite $A\subseteq \mathbb{N}$ is a family $B$ of nonempty finite increasing sequences whose underlying sets are inclusion-incomparable, such that every infinite subset of $A$ has an initial segment in $B$. Write $s◃t$ if both are initial segments of some increasing sequence $u$ and its first-term deletion, respectively. BQO means that every $f:B\to Q$ has $s◃t$ with $f(s){\le }_{Q}f(t)$. Singleton barriers give the WQO condition, so BQO implies WQO. These are the barrier-array conventions explained in the treatment of better-quasi-orders.

The labelled version of Kruskal's tree theorem states that finite rooted trees labelled by a WQO $Q$ are WQO under label-monotone tree embedding. An embedding is an injective vertex map preserving lowest common ancestors and increasing labels. In particular an edge may map to a nonempty path, and the source root may map below the target root. The unlabelled theorem follows by taking one label. We prove the stronger labelled assertion.

We first supply the word lemma needed in the proof. Every sequence in a WQO has an infinite nondecreasing subsequence: color pairs $i<j$ according to whether $q_i\le q_j$ and use Ramsey's theorem; the all-bad homogeneous possibility is excluded by WQO. Suppose finite words over $Q$ had a bad sequence. Choose a minimal bad sequence $w_n$, minimizing length at each stage among choices admitting a bad continuation. No word is empty. Write $w_n=v_n{a}_n$ and choose $n_0<n_1<\cdots$ with $a_{n_r}\le a_{n_s}$ for $r<s$. The sequencecannot be bad by minimality, since its new word at position $n_0$ is shorter. A good pair within the old prefix was already forbidden. A prefix word embedding in some $v_{n_r}$ embeds in $w_{n_r}$, also forbidden. A good pair $v_{n_r}\le v_{n_s}$ extends by the ordered last letters to $w_{n_r}\le w_{n_s}$, again forbidden. This proves the Higman lemma.

Assume next that labelled trees have a bad sequence. Choose $T_n$ minimally by number of vertices, again among choices admitting a bad continuation. Let $\mathcal{S}$ be the collection of all immediate child subtrees of all $T_n$. We claim it is WQO. If $S_0,S_1,\dots$ were a bad sequence in $\mathcal{S}$, attach to each $S_r$ a parent index $k_r$ with $S_r$ a proper child subtree of $T_{k_r}$. The indices must be unbounded on every tail: bounded indices provide only finitely many actual child subtrees, forcing a repeated tree and hence a good pair. Pass to a subsequence with strictly increasing parent indices $k_0<k_1<\cdots$. Thenis bad. Indeed a prefix tree embedding into $S_r$ also embeds into its host $T_{k_r}$, contrary to the original bad sequence, and the other possible good pairs were excluded already. But $S_0$ is smaller than $T_{k_0}$, contradicting minimality. This proves the claim.

Enumerate each tree's child subtrees in any chosen order. Higman's lemma makes the resulting finite words over $\mathcal{S}$ WQO. Products of two WQOs are WQO: choose a nondecreasing subsequence in the first coordinate and then a good pair in the second. Apply this to each root label and child word. Some $i<j$ has an increasing root label and an embedding of its child word into the other's child word. Map the first root to the second root and use the child-subtree embeddings in the matched distinct branches. Their images lie below distinct children, so their pairwise meets are the second root; within each branch the chosen embeddings preserve meets. This gives an embedding $T_i{⪯}_Q{T}_j$, contradicting badness. Hence Kruskal's theorem holds. If one requires roots to be preserved, label the root with a new label incomparable with all ordinary labels and apply the just-proved labelled version; its unique occurrence forces root preservation.

For Friedman's finite form of Kruskal's theorem, fix $k$. Consider bad finite sequences of unlabelled tree isomorphism types satisfying $|T_i|\le k+i$, with indices starting at one. Put them in a tree ordered by extension. At each position there are only finitely many isomorphism types with the allowed vertex bound, so this tree is finitely branching. If bad sequences had arbitrarily large lengths, the König infinity lemma would give an infinite branch, an infinite bad sequence contradicting Kruskal's theorem. ConsequentlyThe bound is uniform over all such sequences. Quotienting by tree isomorphism types is essential to the finite-branching argument; arbitrary vertex names would give infinitely many codes for the same finite tree. A fixed finite label alphabet can be included with the same argument.