In program verification one has often to reason about lists over elements of a given nature. Thus, it becomes important to be able to combine the theory of lists with a generic theory
modeling the elements. This combination can be achieved using the Nelson-Oppen method
is stably infinite.
The goal of this paper is to relax the stable-infiniteness requirement. More specifically, we provide a new method that is able to combine the theory of lists with any theory
of the elements, regardless of whether
is stably infinite or not. The crux of our combination method is to guess an arrangement over a set of variables that is larger than the one considered by Nelson and Oppen.
Furthermore, our results entail that it is also possible to combine
with the more general theory of lists with a length function.