bound a is a if the number of elements in a is lesser or equal to the maximum number of elements allowed, otherwise it is top. Does not bound the size of NotIn, as there are no infinite ascending chains for NotIn.

of_bounds l r is {l, l+1, ..., r} if this set has size up to the maximum number of elements, otherwise it is NotIn {l-1, r+1}. This is a precision optimization compared to simply return top, as we already know that l - 1 and r + 1 will not be in the set of elements. Due to this optimization, top is often represented as ∉{MININT - 1, MAXINT + 1} in C programs.

of_bool t f is:

• ∅ if t = false and f = false
• {0} if t = false and f = true
• {1} if t = true and f = false
• {0,1} if t = true and f = true

combine combiner s1 s2 is {combiner x1 x2 | x1 ∈ s1, x2 ∈ s2}.

*********************

combine_with combiner a1 a2 combines the elements of a1 and a2 with combiner. If a1 and a2 are finite sets, it applies combiner to the cartesian product of the two. If a1 and a2 are both exclued powersets, returns top. If one of the two is a finite set of size exactly one (and therefore, it is a definite value), returns an excluded set where the constant is combined with the excluded powerset. Otherwise, returns top.