• 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

Algebraic Properties

Algebraic Properties

Definitions and Theorems

Theorem: logand-x-0

(defthm logand-x-0
  (equal (logand x 0) 0))

Theorem: logand-0-y

(defthm logand-0-y
  (equal (logand 0 y) 0))

Theorem: logior-x-0

(defthm logior-x-0
  (implies (integerp x)
           (equal (logior x 0) x)))

Theorem: logior-0-y

(defthm logior-0-y
  (implies (integerp y)
           (equal (logior 0 y) y)))

Theorem: logxor-x-0

(defthm logxor-x-0
  (implies (integerp x)
           (equal (logxor x 0) x)))

Theorem: logxor-0-y

(defthm logxor-0-y
  (implies (integerp y)
           (equal (logxor 0 y) y)))

Theorem: logand-self

(defthm logand-self
  (implies (case-split (integerp x))
           (equal (logand x x) x)))

Theorem: logior-self

(defthm logior-self
  (implies (case-split (integerp x))
           (equal (logior x x) x)))

Theorem: logxor-self

(defthm logxor-self
  (equal (logxor x x) 0))

Theorem: lognot-lognot

(defthm lognot-lognot
  (implies (case-split (integerp i))
           (equal (lognot (lognot i)) i)))

Theorem: logior-not-0

(defthm logior-not-0
  (implies (and (integerp x) (integerp y))
           (iff (equal (logior x y) 0)
                (and (= x 0) (= y 0)))))

Theorem: logxor-not-0

(defthm logxor-not-0
  (implies (and (integerp x) (integerp y))
           (iff (equal (logxor x y) 0) (= x y))))

Theorem: logand-x-1

(defthm logand-x-1
  (implies (bvecp x 1)
           (equal (logand x 1) x)))

Theorem: logand-1-x

(defthm logand-1-x
  (implies (bvecp x 1)
           (equal (logand 1 x) x)))

Theorem: logior-1-x

(defthm logior-1-x
  (implies (bvecp x 1)
           (equal (logior 1 x) 1)))

Theorem: logior-x-1

(defthm logior-x-1
  (implies (bvecp x 1)
           (equal (logior x 1) 1)))

Theorem: logand-x-m1

(defthm logand-x-m1
  (implies (integerp x)
           (equal (logand x -1) x)))

Theorem: logand-m1-y

(defthm logand-m1-y
  (implies (integerp y)
           (equal (logand -1 y) y)))

Theorem: logior-x-m1

(defthm logior-x-m1
  (implies (integerp x)
           (equal (logior x -1) -1)))

Theorem: logior-m1-y

(defthm logior-m1-y
  (implies (integerp y)
           (equal (logior -1 y) -1)))

Theorem: logxor-x-m1

(defthm logxor-x-m1
  (implies (integerp x)
           (equal (logxor x -1) (lognot x))))

Theorem: logxor-m1-x

(defthm logxor-m1-x
  (implies (integerp x)
           (equal (logxor -1 x) (lognot x))))

Theorem: logand-commutative

(defthm logand-commutative
  (equal (logand y x) (logand x y)))

Theorem: logior-commutative

(defthm logior-commutative
  (equal (logior y x) (logior x y)))

Theorem: logxor-commutative

(defthm logxor-commutative
  (equal (logxor y x) (logxor x y)))

Theorem: logand-commutative-2

(defthm logand-commutative-2
  (equal (logand y x z) (logand x y z)))

Theorem: logior-commutative-2

(defthm logior-commutative-2
  (equal (logior y x z) (logior x y z)))

Theorem: logxor-commutative-2

(defthm logxor-commutative-2
  (equal (logxor y x z) (logxor x y z)))

Theorem: logand-associative

(defthm logand-associative
  (equal (logand (logand x y) z)
         (logand x (logand y z))))

Theorem: logior-associative

(defthm logior-associative
  (equal (logior (logior x y) z)
         (logior x (logior y z))))

Theorem: logxor-associative

(defthm logxor-associative
  (equal (logxor (logxor x y) z)
         (logxor x (logxor y z))))

Theorem: logior-logand

(defthm logior-logand
  (implies (and (integerp x)
                (integerp y)
                (integerp z))
           (equal (logior x (logand y z))
                  (logand (logior x y) (logior x z)))))

Theorem: logior-logand-1

(defthm logior-logand-1
  (implies (and (integerp x) (integerp y))
           (equal (logior x (logand x y)) x)))

Theorem: logand-logior

(defthm logand-logior
  (implies (and (integerp x)
                (integerp y)
                (integerp z))
           (equal (logand x (logior y z))
                  (logior (logand x y) (logand x z)))))

Theorem: logior-logand-2

(defthm logior-logand-2
  (implies (and (integerp x)
                (integerp y)
                (integerp z))
           (equal (logand (logior y z) x)
                  (logior (logand y x) (logand z x)))))

Theorem: log3

(defthm log3
  (implies (and (integerp x)
                (integerp y)
                (integerp z))
           (equal (logior (logand x y)
                          (logior (logand x z) (logand y z)))
                  (logior (logand x y)
                          (logand (logxor x y) z)))))

Theorem: logxor-rewrite

(defthm logxor-rewrite
  (implies (and (integerp x) (integerp y))
           (equal (logxor x y)
                  (logior (logand x (lognot y))
                          (logand y (lognot x))))))

Theorem: lognot-logxor

(defthm lognot-logxor
  (and (equal (logxor (lognot x) y)
              (lognot (logxor x y)))
       (equal (logxor y (lognot x))
              (lognot (logxor x y)))))