Predicate pointlessComparison

Holds if cmp is a comparison operation that always has the result value, and either

• ss is LeftIsSmaller, and the left hand argument is always at most left, the right hand argument at least right, and left is less than or equal to right; or
• ss is RightIsSmaller, and the left hand argument is always at least left, the right hand argument at most right, and left is greater than or equal to right.

For example, if the comparison x < y is always true because x <= 3 and 5 <= y then pointlessComparison(x < y, 3, 5, true, LeftIsSmaller) holds.

Similarly, if the comparison x < y is always false because x >= 9 and 7 >= y then pointlessComparison(x < y, 9, 7, false, RightIsSmaller) holds.