Proving Termination by Bounded Increase

Jürgen Giesl, René Thiemann, Stephan Swiderski, and Peter Schneider-Kamp

Most methods and tools for termination analysis of term rewrite systems
(TRSs) essentially try to find arguments of functions that decrease
in recursive calls. However, they fail if the reason for termination
is that an argument is increased in recursive calls repeatedly until
it reaches a bound. In this paper, we solve that problem and present a
method to prove termination of TRSs with bounded increase automatically.