plus-and-minus - ACL2 Book

other

(in-package "ACL2")

+-of-+-of---sametheorem

(defthm +-of-+-of---same (equal (+ x (- x) y) (fix y)))

equal-of-0-and-+-of--theorem

(defthm equal-of-0-and-+-of--
  (implies (and (acl2-numberp x) (acl2-numberp y))
    (equal (equal 0 (+ x (- y))) (equal x y))))

equal-of-0-and-+-of---alttheorem

(defthm equal-of-0-and-+-of---alt
  (implies (and (acl2-numberp x) (acl2-numberp y))
    (equal (equal 0 (+ (- y) x)) (equal x y))))

<-of-+-of---and-0-arg2theorem

(defthm <-of-+-of---and-0-arg2
  (equal (< (+ x (- y)) 0) (< x y))
  :hints (("Goal" :cases ((< x y)))))

<-of-+-of---and-0-arg1theorem

(defthm <-of-+-of---and-0-arg1
  (equal (< (+ (- x) y) 0) (< y x))
  :hints (("Goal" :cases ((< y x)))))