Standard rewriting systems on free data structures have limited expressive
power since semantic data structures like sets or multisets cannot be
modeled elegantly.  A class of rewrite systems
that allows the use of semantic data structures is defined.  Additionally, built-in
natural numbers, including (dis)equality, ordering, and divisibility
constraints, are supported for expressing rewrite rules. 
The rewriting 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
very natural way.

One of the most important properties of algorithms and rewrite based
specifications of them is termination.  The
dependency pair framework is extended to be applicable to this class of rewrite systems, thus obtaining a flexible and powerful method for termination proving that can be automated
effectively.