• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
      • Lispfloat
      • Arithmetic-1
        • Inequalities-of-products
        • Basic-product-normalization
        • Inequalities-of-reciprocals
        • Arithmetic/natp-posp
        • Basic-expt-normalization
        • More-rational-identities
        • Inequalities-of-exponents
        • Basic-sum-normalization
        • Basic-rational-identities
        • Basic-expt-type-rules
        • Inequalities-of-sums
        • Basic-products-with-negations
        • Fc
      • Number-theory
      • Proof-by-arith
      • Arith-equivs
      • Include-an-arithmetic-book
      • Number-theory
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra
  • Testing-utilities

• Arithmetic-1
• Expt

Basic-expt-type-rules

Rules about when expt produces integers, positive numbers, etc.

Definitions and Theorems

Theorem: expt-type-prescription-rationalp

(defthm expt-type-prescription-rationalp
  (implies (rationalp r)
           (rationalp (expt r i)))
  :rule-classes (:type-prescription :generalize))

Theorem: expt-type-prescription-positive

(defthm expt-type-prescription-positive
  (implies (and (< 0 r) (real/rationalp r))
           (< 0 (expt r i)))
  :rule-classes (:type-prescription :generalize))

Theorem: expt-type-prescription-nonzero

(defthm expt-type-prescription-nonzero
  (implies (and (fc (acl2-numberp r))
                (not (equal r 0)))
           (not (equal 0 (expt r i))))
  :rule-classes (:type-prescription :generalize))

Theorem: expt-type-prescription-integerp

(defthm expt-type-prescription-integerp
  (implies (and (<= 0 i) (integerp r))
           (integerp (expt r i)))
  :rule-classes (:type-prescription :generalize))