Design new termination methods based on the gap-embedding theorems of Friedman and Kriz.

The source page states the original problem together with its recorded qualifications and progress updates as follows.

Harvey Friedman [Dershowitz, 2002] modified Kruskal's Tree Theorem to restrict labels that appear along the path between the images of adjacent nodes to what is called gap embedding. Whereas Friedman's result applied only to labellings with the natural numbers, Igor K\v{r}'{\i}\v{z} [Dershowitz, 2002] extended it to arbitrary ordinal labellings. See also [Dershowitz, 2002]. The question is whether new and useful termination methods can be based on these gap-embedding theorems. One step in this directions is [Dershowitz, 2002].

This problem is related to RTALooP entry graph-minors.