`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 ‘

`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 + 4 x)`’ holds because the runtime
indeterminate

`known_lt (4, 4 + 4``x`)

nor `known_eq (4, 4 + 4``x`)

hold.