• 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
        • Register-Transfer Logic
          • Bit Vectors
          • Logical Operations
            • Binary Operations
            • Algebraic Properties
            • Complementation
          • Basic Arithmetic Functions
        • Floating-Point Arithmetic
        • Modeling Algorithms in C++ and ACL2
        • Bibliography
    • Algebra
  • Testing-utilities

• Logical Operations

Complementation

Complementation

Definitions and Theorems

Theorem: lognot-def

(defthm lognot-def
  (implies (integerp x)
           (equal (lognot x) (1- (- x)))))

Theorem: lognot-shift

(defthm lognot-shift
  (implies (and (integerp x) (natp k))
           (equal (lognot (* (expt 2 k) x))
                  (+ (* (expt 2 k) (lognot x))
                     (1- (expt 2 k))))))

Theorem: lognot-fl

(defthm lognot-fl
  (implies (and (integerp x) (not (zp n)))
           (equal (lognot (fl (/ x n)))
                  (fl (/ (lognot x) n)))))

Theorem: mod-lognot

(defthm mod-lognot
  (implies (and (integerp x) (natp n))
           (equal (mod (lognot x) (expt 2 n))
                  (1- (- (expt 2 n) (mod x (expt 2 n)))))))

Theorem: bits-lognot

(defthm bits-lognot
  (implies (and (natp i)
                (natp j)
                (<= j i)
                (integerp x))
           (equal (bits (lognot x) i j)
                  (- (1- (expt 2 (- (1+ i) j)))
                     (bits x i j)))))

Theorem: bitn-lognot

(defthm bitn-lognot
  (implies (and (integerp x) (natp n))
           (not (equal (bitn (lognot x) n) (bitn x n))))
  :rule-classes nil)

Theorem: bits-lognot-bits

(defthm bits-lognot-bits
  (implies (and (integerp x)
                (natp i)
                (natp j)
                (natp k)
                (natp l)
                (<= l k)
                (<= k (- i j)))
           (equal (bits (lognot (bits x i j)) k l)
                  (bits (lognot x) (+ k j) (+ l j)))))

Theorem: bits-lognot-bits-lognot

(defthm bits-lognot-bits-lognot
  (implies (and (integerp x)
                (natp i)
                (natp j)
                (natp k)
                (natp l)
                (<= l k)
                (<= k (- i j)))
           (equal (bits (lognot (bits (lognot x) i j))
                        k l)
                  (bits x (+ k j) (+ l j)))))

Theorem: logand-bits-lognot

(defthm logand-bits-lognot
  (implies (and (integerp x)
                (integerp n)
                (bvecp y n))
           (equal (logand y (bits (lognot x) (1- n) 0))
                  (logand y (lognot (bits x (1- n) 0))))))