• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
      • Bv
      • Ihs
      • Rtl
        • Floating-Point Exceptions and Specification of Elementary Arithmetic Instructions
        • Implementation of Elementary Operations
          • Multiplication
          • FMA-Based Division
          • Addition
            • Bit Vector Addition
            • Leading One Prediction
            • Trailing One Prediction
          • SRT Division and Square Root
        • Register-Transfer Logic
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Addition

Trailing One Prediction

Trailing One Prediction

Definitions and Theorems

Theorem: top-thm-1

(defthm top-thm-1
  (implies (and (natp k) (integerp a) (integerp b))
           (equal (equal (bits (+ a b 1) k 0) 0)
                  (equal (bits (lognot (logxor a b)) k 0)
                         0)))
  :rule-classes nil)

Theorem: top-thm-2

(defthm top-thm-2
  (implies (and (natp n)
                (integerp a)
                (integerp b)
                (natp k)
                (< k n)
                (or (equal c 0) (equal c 1)))
           (equal (equal (bits (+ a b c) k 0) 0)
                  (equal (bits (logxor (logxor a b)
                                       (cat (logior a b) n c 1))
                               k 0)
                         0)))
  :rule-classes nil)