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 equational completion procedures.

**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.

© 1996-9

1999-05-26