Transforming Termination by Self-Labelling

We introduce a new technique for proving termination of term rewriting systems. The technique, a $\mathrm{s}\mathrm{p}\mathrm{e}\mathrm{c}\mathrm{i}\mathrm{a}$] $\mathrm{i}_{\mathrm{Z}}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n} $ of Zantelna’s semantic labelling technique, is especially useful for establishing the correctness of transformation methods that attempt to prove termination by transforlning $\mathrm{t}\mathrm{e}\mathrm{r}\ln $ rewriting $\mathrm{s}\mathrm{y}\mathrm{s}\iota \mathrm{e}\mathrm{l}\mathrm{n}\mathrm{S} $ into systems whose termination is $\mathrm{e}\mathrm{a}s$ier to prove. We apply the technique to distribution elimination, dummy elimination, and currying, resulting in shorter correctness prook, stronger results, and a positive solution to an open problem. 1