 Kruskal's tree theorem

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.

Kruskal's tree theorem is a result in graph theory and combinatorics that deals with the structure of trees and their embeddings within each other. More specifically, it provides criteria for the comparison and embedding of trees.