		Search-engine friendly clone of the ACL2 documentation.

Basic-sum-normalization

Trivial normalization and cancellation rules for sums.

Theorem: functional-self-inversion-of-minus

(defthm functional-self-inversion-of-minus
  (equal (- (- x)) (fix x)))

Theorem: minus-cancellation-on-right

(defthm minus-cancellation-on-right
  (equal (+ x y (- x)) (fix y)))

Theorem: minus-cancellation-on-left

(defthm minus-cancellation-on-left
  (equal (+ x (- x) y) (fix y)))

Theorem: right-cancellation-for-+

(defthm right-cancellation-for-+
  (equal (equal (+ x z) (+ y z))
         (equal (fix x) (fix y))))

Theorem: left-cancellation-for-+

(defthm left-cancellation-for-+
  (equal (equal (+ x y) (+ x z))
         (equal (fix y) (fix z))))

Theorem: equal-minus-0

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

Theorem: inverse-of-+-as=0

(defthm inverse-of-+-as=0
  (equal (equal (- a b) 0)
         (equal (fix a) (fix b))))

Theorem: equal-minus-minus

(defthm equal-minus-minus
  (equal (equal (- a) (- b))
         (equal (fix a) (fix b))))