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