• 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

Inequalities-of-exponents

Rules for resolving inequalities between exponents.

Definitions and Theorems

Theorem: expt->-1

(defthm expt->-1
        (implies (and (< 1 r)
                      (< 0 i)
                      (fc (real/rationalp r))
                      (fc (integerp i)))
                 (< 1 (expt r i)))
        :rule-classes :linear)

Theorem: expt-is-increasing-for-base>1

(defthm expt-is-increasing-for-base>1
        (implies (and (< 1 r)
                      (< i j)
                      (fc (real/rationalp r))
                      (fc (integerp i))
                      (fc (integerp j)))
                 (< (expt r i) (expt r j)))
        :rule-classes (:rewrite :linear))

Theorem: expt-is-decreasing-for-pos-base<1

(defthm expt-is-decreasing-for-pos-base<1
        (implies (and (< 0 r)
                      (< r 1)
                      (< i j)
                      (fc (real/rationalp r))
                      (fc (integerp i))
                      (fc (integerp j)))
                 (< (expt r j) (expt r i))))

Theorem: expt-is-weakly-increasing-for-base>1

(defthm expt-is-weakly-increasing-for-base>1
        (implies (and (< 1 r)
                      (<= i j)
                      (fc (real/rationalp r))
                      (fc (integerp i))
                      (fc (integerp j)))
                 (<= (expt r i) (expt r j))))

Theorem: expt-is-weakly-decreasing-for-pos-base<1

(defthm expt-is-weakly-decreasing-for-pos-base<1
        (implies (and (< 0 r)
                      (< r 1)
                      (<= i j)
                      (fc (real/rationalp r))
                      (fc (integerp i))
                      (fc (integerp j)))
                 (<= (expt r j) (expt r i))))