A basic theory of algebra for all INTEGERPs.
this theory consists of the ACL2-numberp-algebra and rationalp-algebra theories, along with additional lemmas about the integers.