10.3.2 Properties of the poly_int comparisons

All “maybe” relations except maybe_ne are transitive, so for example:

maybe_lt (a, b) && maybe_lt (b, c) implies maybe_lt (a, c)

for all a, b and c. maybe_lt, maybe_gt and maybe_ne are irreflexive, so for example:

!maybe_lt (a, a)

is true for all a. maybe_le, maybe_eq and maybe_ge are reflexive, so for example:

maybe_le (a, a)

is true for all a. maybe_eq and maybe_ne are symmetric, so:

maybe_eq (a, b) == maybe_eq (b, a)
maybe_ne (a, b) == maybe_ne (b, a)

for all a and b. In addition:

maybe_le (a, b) == maybe_lt (a, b) || maybe_eq (a, b)
maybe_ge (a, b) == maybe_gt (a, b) || maybe_eq (a, b)
maybe_lt (a, b) == maybe_gt (b, a)
maybe_le (a, b) == maybe_ge (b, a)

However:

maybe_le (a, b) && maybe_le (b, a) does not imply !maybe_ne (a, b) [== known_eq (a, b)]
maybe_ge (a, b) && maybe_ge (b, a) does not imply !maybe_ne (a, b) [== known_eq (a, b)]

One example is again ‘a == 3 + 4x’ and ‘b == 1 + 5x’, where ‘maybe_le (a, b)’, ‘maybe_ge (a, b)’ and ‘maybe_ne (a, b)’ all hold. maybe_le and maybe_ge are therefore not antisymetric and do not form a partial order.

From the above, it follows that:

• All “known” relations except known_ne are transitive.
• known_lt, known_ne and known_gt are irreflexive.
• known_le, known_eq and known_ge are reflexive.

Also:

known_lt (a, b) == known_gt (b, a)
known_le (a, b) == known_ge (b, a)
known_lt (a, b) implies !known_lt (b, a)  [asymmetry]
known_gt (a, b) implies !known_gt (b, a)
known_le (a, b) && known_le (b, a) == known_eq (a, b) [== !maybe_ne (a, b)]
known_ge (a, b) && known_ge (b, a) == known_eq (a, b) [== !maybe_ne (a, b)]

known_le and known_ge are therefore antisymmetric and are partial orders. However:

known_le (a, b) does not imply known_lt (a, b) || known_eq (a, b)
known_ge (a, b) does not imply known_gt (a, b) || known_eq (a, b)

For example, ‘known_le (4, 4 + 4x)’ holds because the runtime indeterminate x is a nonnegative integer, but neither known_lt (4, 4 + 4x) nor known_eq (4, 4 + 4x) hold.