		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))))