• 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
            • Expt-algebra
            • Integerp-algebra
          • 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

Expt-algebra

A theory of EXPT which is compatible with the ALGEBRA theories.

This theory contains :TYPE-PRESCRIPTIONS, simpification, normalization and selected :LINEAR rules for expt. This theory will not be useful unless the integerp-algebra theory, or something similar is ENABLEd.