• 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

Binary Operations

Binary Operations

Definitions and Theorems

Theorem: logand-def

(defthm logand-def
  (equal (logand x y)
         (if (or (zip x) (zip y))
             0
           (if (= x y)
               x
             (+ (* 2 (logand (fl (/ x 2)) (fl (/ y 2))))
                (logand (mod x 2) (mod y 2))))))
  :rule-classes
  ((:definition :controller-alist ((binary-logand t t)))))

Theorem: logior-def

(defthm logior-def
  (implies (and (integerp x) (integerp y))
           (equal (logior x y)
                  (if (or (zip x) (= x y))
                      y
                    (if (zip y)
                        x
                      (+ (* 2 (logior (fl (/ x 2)) (fl (/ y 2))))
                         (logior (mod x 2) (mod y 2)))))))
  :rule-classes
  ((:definition :controller-alist ((binary-logior t t)))))

Theorem: logxor-def

(defthm logxor-def
  (implies (and (integerp x) (integerp y))
           (equal (logxor x y)
                  (if (zip x)
                      y
                    (if (zip y)
                        x
                      (if (= x y)
                          0
                        (+ (* 2 (logxor (fl (/ x 2)) (fl (/ y 2))))
                           (logxor (mod x 2) (mod y 2))))))))
  :rule-classes
  ((:definition :controller-alist ((binary-logxor t t)))))

Function: log-induct

(defun log-induct (x y)
  (if (or (not (integerp x))
          (not (integerp y))
          (= x 0)
          (= y 0)
          (= x y))
      (+ x y)
    (log-induct (fl (/ x 2)) (fl (/ y 2)))))

Theorem: logand-bvecp

(defthm logand-bvecp
  (implies (and (natp n) (bvecp x n) (integerp y))
           (bvecp (logand x y) n)))

Theorem: logior-bvecp

(defthm logior-bvecp
  (implies (and (bvecp x n) (bvecp y n))
           (bvecp (logior x y) n)))

Theorem: logxor-bvecp

(defthm logxor-bvecp
  (implies (and (bvecp x n) (bvecp y n) (natp n))
           (bvecp (logxor x y) n)))

Theorem: logand-plus-logxor

(defthm logand-plus-logxor
  (implies (and (integerp x) (integerp y))
           (equal (+ (logand x y) (logxor x y))
                  (logior x y))))

Theorem: logand-mod

(defthm logand-mod
  (implies (and (integerp x)
                (integerp y)
                (integerp n))
           (equal (mod (logand x y) (expt 2 n))
                  (logand (mod x (expt 2 n))
                          (mod y (expt 2 n))))))

Theorem: logior-mod

(defthm logior-mod
  (implies (and (integerp x)
                (integerp y)
                (integerp n))
           (equal (mod (logior x y) (expt 2 n))
                  (logior (mod x (expt 2 n))
                          (mod y (expt 2 n))))))

Theorem: logxor-mod

(defthm logxor-mod
  (implies (and (integerp x)
                (integerp y)
                (integerp n))
           (equal (mod (logxor x y) (expt 2 n))
                  (logxor (mod x (expt 2 n))
                          (mod y (expt 2 n))))))

Theorem: fl-logand

(defthm fl-logand
  (implies (and (integerp x) (integerp y) (natp n))
           (equal (fl (* (expt 2 (- n)) (logand x y)))
                  (logand (fl (* (expt 2 (- n)) x))
                          (fl (* (expt 2 (- n)) y))))))

Theorem: fl-logior

(defthm fl-logior
  (implies (and (integerp x) (integerp y) (natp n))
           (equal (fl (* (expt 2 (- n)) (logior x y)))
                  (logior (fl (* (expt 2 (- n)) x))
                          (fl (* (expt 2 (- n)) y))))))

Theorem: fl-logxor

(defthm fl-logxor
  (implies (and (integerp x) (integerp y) (natp n))
           (equal (fl (* (expt 2 (- n)) (logxor x y)))
                  (logxor (fl (* (expt 2 (- n)) x))
                          (fl (* (expt 2 (- n)) y))))))

Theorem: logand-cat

(defthm logand-cat
  (implies (and (case-split (integerp x1))
                (case-split (integerp y1))
                (case-split (integerp x2))
                (case-split (integerp y2))
                (case-split (natp n))
                (case-split (natp m)))
           (equal (logand (cat x1 m y1 n) (cat x2 m y2 n))
                  (cat (logand x1 x2)
                       m (logand y1 y2)
                       n))))

Theorem: logior-cat

(defthm logior-cat
  (implies (and (case-split (integerp x1))
                (case-split (integerp y1))
                (case-split (integerp x2))
                (case-split (integerp y2))
                (case-split (natp n))
                (case-split (natp m)))
           (equal (logior (cat x1 m y1 n) (cat x2 m y2 n))
                  (cat (logior x1 x2)
                       m (logior y1 y2)
                       n))))

Theorem: logxor-cat

(defthm logxor-cat
  (implies (and (case-split (integerp x1))
                (case-split (integerp y1))
                (case-split (integerp x2))
                (case-split (integerp y2))
                (case-split (natp n))
                (case-split (natp m)))
           (equal (logxor (cat x1 m y1 n) (cat x2 m y2 n))
                  (cat (logxor x1 x2)
                       m (logxor y1 y2)
                       n))))

Theorem: logand-shift

(defthm logand-shift
  (implies (and (integerp x) (integerp y) (natp k))
           (equal (logand (* (expt 2 k) x)
                          (* (expt 2 k) y))
                  (* (expt 2 k) (logand x y)))))

Theorem: logior-shift

(defthm logior-shift
  (implies (and (integerp x) (integerp y) (natp k))
           (equal (logior (* (expt 2 k) x)
                          (* (expt 2 k) y))
                  (* (expt 2 k) (logior x y)))))

Theorem: logxor-shift

(defthm logxor-shift
  (implies (and (integerp x) (integerp y) (natp k))
           (equal (logxor (* (expt 2 k) x)
                          (* (expt 2 k) y))
                  (* (expt 2 k) (logxor x y)))))

Theorem: logand-expt

(defthm logand-expt
  (implies (and (integerp x) (integerp y) (natp n))
           (equal (logand (* (expt 2 n) x) y)
                  (* (expt 2 n)
                     (logand x (fl (/ y (expt 2 n))))))))

Theorem: logior-expt

(defthm logior-expt
  (implies (and (integerp x) (integerp y) (natp n))
           (equal (logior (* (expt 2 n) x) y)
                  (+ (* (expt 2 n)
                        (logior x (fl (/ y (expt 2 n)))))
                     (mod y (expt 2 n))))))

Theorem: logxor-expt

(defthm logxor-expt
  (implies (and (integerp x) (integerp y) (natp n))
           (equal (logxor (* (expt 2 n) x) y)
                  (+ (* (expt 2 n)
                        (logxor x (fl (/ y (expt 2 n)))))
                     (mod y (expt 2 n))))))

Theorem: logior-expt-cor

(defthm logior-expt-cor
  (implies (and (natp n) (integerp x) (bvecp y n))
           (equal (logior (* (expt 2 n) x) y)
                  (+ (* (expt 2 n) x) y))))

Theorem: logior-2**n

(defthm logior-2**n
  (implies (and (natp n) (integerp x))
           (equal (logior (expt 2 n) x)
                  (if (= (bitn x n) 1)
                      x
                    (+ x (expt 2 n))))))

Theorem: logand-bits

(defthm logand-bits
  (implies (and (integerp x)
                (natp n)
                (natp k)
                (< k n))
           (equal (logand x (- (expt 2 n) (expt 2 k)))
                  (* (expt 2 k) (bits x (1- n) k)))))

Theorem: logand-bit

(defthm logand-bit
  (implies (and (integerp x) (natp n))
           (equal (logand x (expt 2 n))
                  (* (expt 2 n) (bitn x n)))))

Theorem: bits-logand

(defthm bits-logand
  (implies (and (integerp x)
                (integerp y)
                (integerp i)
                (integerp j))
           (equal (bits (logand x y) i j)
                  (logand (bits x i j) (bits y i j)))))

Theorem: bits-logior

(defthm bits-logior
  (implies (and (integerp x)
                (integerp y)
                (integerp i)
                (integerp j))
           (equal (bits (logior x y) i j)
                  (logior (bits x i j) (bits y i j)))))

Theorem: bits-logxor

(defthm bits-logxor
  (implies (and (integerp x)
                (integerp y)
                (integerp i)
                (integerp j))
           (equal (bits (logxor x y) i j)
                  (logxor (bits x i j) (bits y i j)))))

Theorem: bitn-logand

(defthm bitn-logand
  (implies (and (integerp x)
                (integerp y)
                (integerp n))
           (equal (bitn (logand x y) n)
                  (logand (bitn x n) (bitn y n)))))

Theorem: bitn-logior

(defthm bitn-logior
  (implies (and (integerp x)
                (integerp y)
                (integerp n))
           (equal (bitn (logior x y) n)
                  (logior (bitn x n) (bitn y n)))))

Theorem: bitn-logxor

(defthm bitn-logxor
  (implies (and (case-split (integerp x))
                (case-split (integerp y))
                (case-split (integerp n)))
           (equal (bitn (logxor x y) n)
                  (logxor (bitn x n) (bitn y n)))))