• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
      • 100-theorems
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
        • Bv
        • Ihs
          • Logops-definitions
          • Math-lemmas
            • Prefer-*-to-/
            • ACL2-numberp-algebra
            • Integerp-+-minus-*
            • Rewrite-linear-equalities-to-iff
            • Ihs-math
            • Rationalp-algebra
            • Normalize-<-/-to-*-3
            • Expt-algebra
            • Cancel-equal-+-*
            • Normalize-<-/-to-*
            • Normalize-<-minus-/
            • Normalize-equal-/-to-*
            • Normalize-equal-0
            • Integerp-algebra
            • Ihs-theories
            • Ihs-init
            • Logops
          • Rtl
        • Algebra
      • Testing-utilities
    • Math-lemmas
    • Ihs-math

    Integerp-algebra

    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.