• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
        • Logops-definitions
        • Math-lemmas
          • Prefer-*-to-/
          • ACL2-numberp-algebra
          • Integerp-+-minus-*
          • Rewrite-linear-equalities-to-iff
          • Normalize-<-/-to-*-3
          • Ihs-math
          • Rationalp-algebra
          • Normalize-<-/-to-*
          • Expt-algebra
          • Cancel-equal-+-*
          • Normalize-<-minus-/
          • Normalize-equal-/-to-*
          • Normalize-equal-0
          • Integerp-algebra
        • Ihs-theories
        • Ihs-init
        • Logops
      • Rtl
    • Algebra

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