• 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
      • 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-sums

Basic normalization to move negative terms to the other side of an inequality.

Definitions and Theorems

Theorem: <-0-minus

(defthm <-0-minus (equal (< 0 (- x)) (< x 0)))

Theorem: <-minus-zero

(defthm <-minus-zero
        (equal (< (- x) 0) (< 0 x)))

Theorem: <-0-+-negative-1

(defthm <-0-+-negative-1
        (equal (< 0 (+ (- y) x)) (< y x)))

Theorem: <-0-+-negative-2

(defthm <-0-+-negative-2
        (equal (< 0 (+ x (- y))) (< y x)))

Theorem: <-+-negative-0-1

(defthm <-+-negative-0-1
        (equal (< (+ (- y) x) 0) (< x y)))

Theorem: <-+-negative-0-2

(defthm <-+-negative-0-2
        (equal (< (+ x (- y)) 0) (< x y)))