Module Arith_int.MakeSource

cancellative superposition where given clause is active

cancellative superposition where given clause is passive

cancellation (unifies some terms on both sides of a comparison operator)

cancellative equality factoring

cancellative inequality chaining.

Also does case switch if conditions are present: C1 or a < b C2 or b < c ------------------------------------- C1 or C2 or or_=a+1....c-1 (b = i) if a and c are integer linear expressions whose difference is a constant. If a > c, then the range a...c is empty and the literal is just removed.

Factoring between two inequation literals

Simplification: a < b ----> a+1 ≤ b

Chain together two divisibility literals, assuming they share the same prime

Eliminate negative divisibility literals within a power-of-prime quotient of Z: not (d^i | m) ----->

Eliminate divisibility literals with a non-power-of-prime quotient of Z (for instance 6 | a ---> { 2 | a, 3 | a })

Infer divisibility constraints from integer equations, for instance C or 2a=b ----> C or 2 | b if a is maximal

is the clause a tautology w.r.t linear expressions?

Eliminate unshielded variables using an adaptation of Cooper's algorithm