ABSTRACT
A class of theories presented by constructor-based convergent rewrite systems with decidable matching problem is characterized by means of some semantic requirements on the rewrite system. Such requirements are satisfied whenever in any reduction each recursive call to a function occurs into a term in a position such that the term is P increasing at that position, P being a property of terms like depth, size, and so on. The P increase property enables a sorting of the equations generated during the execution of the adopted matching procedure according to a well-founded ordering.
