A theorem which 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.
Kruskal's Tree Theorem
See also
Knuth-Bendix Completion Algorithm, König's Lemma, Kruskal's Algorithm, Natural Independence Phenomenon, TreeExplore with Wolfram|Alpha
References
Gallier, J. "What's so Special about Kruskal's Theorem and the Ordinal Gamma[0]? A Survey of Some Results in Proof Theory." Ann. Pure and Appl. Logic 53, 199-260, 1991.Referenced on Wolfram|Alpha
Kruskal's Tree TheoremCite this as:
Weisstein, Eric W. "Kruskal's Tree Theorem." From MathWorld--A Wolfram Web Resource. https://mathworld.wolfram.com/KruskalsTreeTheorem.html