		Search-engine friendly clone of the ACL2 documentation.

Math-lemmas

Normalize-equal-0

Rewrite (equal (- x) 0), (equal (+ x y) 0), and (equal (* x y) 0).

Definitions and Theorems

Theorem: normalize-equal-0

(defthm normalize-equal-0
  (and (equal (equal (- x) 0)
              (equal (fix x) 0))
       (equal (equal (+ x y) 0)
              (equal (fix x) (- y)))
       (equal (equal (* x y) 0)
              (or (equal (fix x) 0)
                  (equal (fix y) 0)))))