A book of theories about +, -, *, /, and EXPT, built on the
arithmetic package of Matt Kaufmann.
- A small theory of lemmas that eliminate / in favor of *.
- A basic theory of algebra for all ACL2-numberps.
- Rewrite: -i, i + j, i - j, and i * j are integers, when i and j are
- Rewrite: (EQUAL (< w x) (< y z)) → (IFF (< w x) (< y z)).
- Rewrite: Replace x < y/z and x > y/z with x*z < y or
x*z > y, depending on the sign of z.
- The default theory of +, -, *, /, and EXPT for the IHS library.
- A basic theory of algebra for all rationalps.
- Rewrite: Replace x < 1/y with x*y < 1 or x*y > 1,
based on the sign of y.
- A theory of EXPT which is compatible with the ALGEBRA theories.
- Rewrite: (equal (+ x y) x) and (equal (* x y) x);
also commutative forms.
- Rewrite inequalities between 0 and negated or reciprocal terms, and
(< (- x) (- y)).
- Rewrite: Replace x = y/z with x*z = y.
- Rewrite (equal (- x) 0), (equal (+ x y) 0), and
(equal (* x y) 0).
- A basic theory of algebra for all INTEGERPs.