  In the dependency pair framework for proving termination of rewriting
systems, polynomial interpretations are used to transform dependency chains
into bounded decreasing sequences of integers, and they play an important role
for the success of proving termination, especially for constrained rewriting
systems. In this paper, we show sufficient conditions of linear polynomial
interpretations for transforming dependency chains into bounded monotone (i.e.,
decreasing or increasing) sequences of integers. Such polynomial
interpretations transform rewrite sequences of the original system into
decreasing or increasing sequences independently of the transformation of
dependency chains. When we transform rewrite sequences into increasing
sequences, polynomial interpretations have non-positive coefficients for
reducible positions of marked function symbols. We propose four DP processors
parameterized by transforming dependency chains and rewrite sequences into
either decreasing or increasing sequences of integers, respectively. We show
that such polynomial interpretations make us succeed in proving termination of
the McCarthy 91 function over the integers.
