Using unavoidable set of trees to generalize Kruskal's theorem (Q1122597)

Termination is an important property for term rewriting systems. To prove termination, \textit{N. Dershowitz} [Theor. Comput. Sci. 17, 279-301 (1982; Zbl 0525.68054)] introduces quasi-simplification orderings that are monotonic extensions of the embedding relation. He proves that they are well quasi-ordered and a fortiori well-founded by using a theorem of \textit{J. B. Kruskal} [Trans. Am. Math. Soc. 95, 210-225 (1960; Zbl 0158.270)], which shows that the simple tree insertion order TIO (defined below) is a well quasi-ordering over a certain set of trees. (Well-founded means that every nonempty set contains at least one minimal element; well quasi- ordered means that every nonempty set contains at least one and at most a finite number of noncomparable minimal elements.) Dershowitz's method is powerful, but cannot be used when the rewriting system contains a rule whose right hand side is embedded in the left hand side. The purpose of this paper is to overcome this constraint, when the rewriting system uses a finite ranked alphabet, by generalizing Kruskal's theorem to obtain a family of quasi-orders TIO(S,\(\omega)\) that are strictly included in TIO but are still well quasi-orders.