The abstract type representing sets that we want to refine.

is_empty s determines whether the set s is empty.

Total ordering.

compare_minimum s1 s2 compares the nonempty sets s1 and s2 based on their minimum elements.

sorted_union ss computes the union of all sets in the list ss. Every set in the list ss must be nonempty. The intervals that underlie these sets must be ordered and nonoverlapping: that is, if s1 and s2 are two adjacent sets in the list ss, then they must satisfy the condition maximum s1 < minimum s2.

extract_unique_prefix s1 s2 requires compare_minimum s1 s2 < 0, that is, minimum s1 < minimum s2. It splits s1 in two disjoint subsets head1 and tail1 such that head1 is exactly the subset of s1 whose elements are less than minimum s2. Therefore, head1 must be nonempty, whereas tail1 may be empty.

extract_shared_prefix s1 s2 requires compare_minimum s1 s2 = 0, that is, minimum s1 = minimum s2. It splits s1 and s2 into three subsets head, tail1, and tail2, as follows:

• s1 is head U tail1 and s2 is head U tail2. This implies that head is a subset of both s1 and s2.
• An element in head is smaller than every element in tail1 and tail2.
• head is maximal with respect to the previous two properties.

In summary, head is the maximal shared prefix of the sets s1 and s2.