		Search-engine friendly clone of the ACL2 documentation.

Math-lemmas

Cancel-equal-+-*

Rewrite: (equal (+ x y) x) and (equal (* x y) x); also commutative forms.

Definitions and Theorems

Theorem: cancel-equal-+-*

(defthm cancel-equal-+-*
  (and (equal (equal (+ x y) x)
              (and (acl2-numberp x)
                   (equal (fix y) 0)))
       (equal (equal (+ y x) x)
              (and (acl2-numberp x)
                   (equal (fix y) 0)))
       (equal (equal (* x y) x)
              (and (acl2-numberp x)
                   (or (equal x 0) (equal y 1))))
       (equal (equal (* x y) y)
              (and (acl2-numberp y)
                   (or (equal y 0) (equal x 1))))))