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

• Math-lemmas

Rationalp-algebra

A basic theory of algebra for all rationalps.

This theory includes the ACL2-numberp-algebra theory along with additional lemmas about the rationals.

This theory extends ACL2-NUMBERP-ALGEBRA to include theorems about NUMERATOR and DENOMINATOR, and simple cancellation and normalization theorems and other simple theorems for inequalities.