  Size-Change Termination (SCT) is a method of proving program termination
based on the impossibility of infinite descent. To this end we use a program
abstraction in which transitions are described by Monotonicity Constraints over
(abstract) variables. When only constraints of the form x>y' and x\geq y' are
allowed, we have size-change graphs. In the last decade, both theory and
practice have evolved significantly in this restricted framework. The crucial
underlying assumption of most of the past work is that the domain of the
variables is well-founded. In a recent paper I showed how to extend and adapt
some theory from the domain of size-change graphs to general monotonicity
constraints, thus complementing previous work, but remaining in the realm of
well-founded domains. However, monotonicity constraints are, interestingly,
capable of proving termination also in the integer domain, which is not
well-founded. The purpose of this paper is to explore the application of
monotonicity constraints in this domain. We lay the necessary theoretical
foundation, and present precise decision procedures for termination; finally,
we provide a procedure to construct explicit global ranking functions from
monotonicity constraints in singly-exponential time, and of optimal worst-case
size and dimension (ordinal).
