Kruskal's tree theorem
= Kruskal's tree theorem
{c}
{wiki}
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.