• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • 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
• Prefer-*-to-/

Normalize-equal-/-to-*

Rewrite: Replace x = y/z with x*z = y.

Definitions and Theorems

Theorem: normalize-equal-/-to-*

(defthm normalize-equal-/-to-*
        (implies (and (acl2-numberp z) (not (equal z 0)))
                 (and (equal (equal x (* y (/ z)))
                             (and (acl2-numberp x)
                                  (equal (* x z) (fix y))))
                      (equal (equal x (* (/ z) y))
                             (and (acl2-numberp x)
                                  (equal (* x z) (fix y)))))))