Rewrite systems on free data structures have limited expressive power since semantic data structures like sets or multisets cannot be modeled elegantly. In this work we define a class of rewrite systems that allows the use of semantic data structures. Additionally, built-in natural numbers, including (dis)equality, ordering, and divisibility constraints, are supported. The rewrite mechanism is a combination of normalized equational rewriting with validity checking of instantiated constraints. The framework is highly expressive and allows modeling of algorithms in a natural way.

Termination is one of the most important properties of algorithms. This is true for both functional programs and imperative programs operating on natural numbers, which can be translated into rewrite systems. In this work, the dependency pair framework for proving termination is extended to be applicable to the class of rewrite systems described above, thus obtaining a flexible and powerful method for showing termination that can be automated effectively. We develop various refinements which increase power and efficiency of the method.