• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • 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
      • Number-theory
      • Arithmetic-3
      • Arithmetic-2
      • Arithmetic-light
      • Arithmetic-5
    • Bit-vectors
    • Algebra

• Arithmetic-1
• Expt

Basic-expt-normalization

Basic rules for normalizing and simplifying exponents.

Definitions and Theorems

Theorem: right-unicity-of-1-for-expt

(defthm right-unicity-of-1-for-expt
        (equal (expt r 1) (fix r)))

Theorem: expt-minus

(defthm expt-minus
        (equal (expt r (- i)) (/ (expt r i))))

Theorem: exponents-add-for-nonneg-exponents

(defthm exponents-add-for-nonneg-exponents
        (implies (and (<= 0 i)
                      (<= 0 j)
                      (fc (integerp i))
                      (fc (integerp j)))
                 (equal (expt r (+ i j))
                        (* (expt r i) (expt r j)))))

Theorem: exponents-add

(defthm exponents-add
        (implies (and (syntaxp (not (and (quotep i)
                                         (integerp (cadr i))
                                         (or (equal (cadr i) 1)
                                             (equal (cadr i) -1)))))
                      (syntaxp (not (and (quotep j)
                                         (integerp (cadr j))
                                         (or (equal (cadr j) 1)
                                             (equal (cadr j) -1)))))
                      (not (equal 0 r))
                      (fc (acl2-numberp r))
                      (fc (integerp i))
                      (fc (integerp j)))
                 (equal (expt r (+ i j))
                        (* (expt r i) (expt r j)))))

Theorem: exponents-add-unrestricted

(defthm exponents-add-unrestricted
        (implies (and (not (equal 0 r))
                      (fc (acl2-numberp r))
                      (fc (integerp i))
                      (fc (integerp j)))
                 (equal (expt r (+ i j))
                        (* (expt r i) (expt r j)))))

Theorem: distributivity-of-expt-over-*

(defthm distributivity-of-expt-over-*
        (equal (expt (* a b) i)
               (* (expt a i) (expt b i))))

Theorem: expt-1

(defthm expt-1 (equal (expt 1 x) 1))

Theorem: exponents-multiply

(defthm exponents-multiply
        (implies (and (fc (integerp i))
                      (fc (integerp j)))
                 (equal (expt (expt r i) j)
                        (expt r (* i j)))))

Theorem: functional-commutativity-of-expt-/-base

(defthm functional-commutativity-of-expt-/-base
        (equal (expt (/ r) i) (/ (expt r i))))

Theorem: equal-constant-+

(defthm equal-constant-+
        (implies (syntaxp (and (quotep c1) (quotep c2)))
                 (equal (equal (+ c1 x) c2)
                        (if (acl2-numberp c2)
                            (if (acl2-numberp x)
                                (equal x (- c2 c1))
                                (equal (fix c1) c2))
                            nil))))