Kruskal's tree theorem states that every infinite sequence of finite unordered rooted trees with labels from
a fixed finite set contains an earlier rooted tree
that admits a label-preserving injection into a later
one preserving meets in the ancestry orders. Here 
means that 
lies on the path from the root
to 
, including its endpoints. The injection
need not preserve the root. Labels in this version are compared for equality
(Gallier 1991). The TREE function measures the greatest
possible length of sequences without such a pair under
an indexed bound on the number of vertices.
Kruskal's tree theorem plays a fundamental role in computer science because it is one of the main tools for showing that certain orderings on trees are well-founded. These orderings play a crucial role in proving the termination of rewriting rules and the correctness of the Knuth-Bendix completion algorithm.
? A Survey of Some Results in Proof Theory." Ann.
Pure and Appl. Logic 53, 199-260, 1991.