logand - ACL2 Book

Included Books

building-blocks top more-floor-mod floor-mod floor-mod-basic truncate-rem logand-helper

other

(in-package "ACL2")

include-book

(include-book "../basic-ops/building-blocks")

local

(local (include-book "../basic-ops/top"))

local

(local (include-book "more-floor-mod"))

local

(local (include-book "floor-mod"))

local

(local (include-book "floor-mod-basic"))

local

(local (include-book "truncate-rem"))

local

(local (include-book "logand-helper"))

local

(local (set-default-hints '((nonlinearp-default-hint++ id
       stable-under-simplificationp
       hist
       nil))))

local

(local (in-theory (e/d (ash-to-floor) (ash))))

local

(local (in-theory (disable not-integerp-type-set-rules
      expt-type-prescription-nonpositive-base-odd-exponent
      expt-type-prescription-nonpositive-base-even-exponent
      expt-type-prescription-negative-base-odd-exponent
      expt-type-prescription-negative-base-even-exponent
      expt-type-prescription-integerp-base
      expt-type-prescription-positive-base
      expt-type-prescription-integerp-base-b
      expt-type-prescription-integerp-base-a
      default-plus-1
      default-plus-2
      default-times-1
      default-times-2
      default-floor-ratio
      default-divide
      default-minus
      cancel-floor-+
      |(floor (+ x r) i)|
      mod-positive
      mod-negative
      mod-nonpositive
      floor-nonnegative
      floor-negative
      floor-positive
      floor-nonpositive
      rationalp-x
      integerp-/-expt-2
      the-floor-below
      |(equal c (- x))|
      (:rewrite floor-x-y-=-1 . 2)
      (:rewrite mod-x-y-=-x+y . 1)
      default-less-than-1
      default-expt-1
      default-expt-2
      default-floor-1
      default-floor-2
      default-mod-2
      mod-bounds-2
      floor-zero
      mod-zero
      mod-x-y-=-x
      mod-x-y-=-x-y)))

|(logand y x)|theorem

(defthm |(logand y x)| (equal (logand y x) (logand x y)))

|(logand (logand x y) z)|theorem

(defthm |(logand (logand x y) z)|
  (equal (logand (logand x y) z) (logand x y z)))

|(logand y x z)|theorem

(defthm |(logand y x z)|
  (equal (logand y x z) (logand x y z))
  :hints (("Goal" :use (:instance logand-y-x-z))))

|(logand c d x)|theorem

(defthm |(logand c d x)|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (logand c d x) (logand (logand c d) x))))

logand-0-xtheorem

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

|(logand 1 x)|theorem

(defthm |(logand 1 x)|
  (implies (integerp x)
    (equal (logand 1 x)
      (if (evenp x)
        0
        1)))
  :hints (("Goal" :expand ((logand 1 x) (logand 0 (floor x 2))))))

logand--1-xtheorem

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

logand-x-xtheorem

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

logand-bounds-postheorem

(defthm logand-bounds-pos
  (implies (and (integerp x) (integerp y) (<= 0 x))
    (<= (logand x y) x))
  :hints (("Goal" :in-theory (enable logand)))
  :rule-classes ((:rewrite) (:linear)
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (<= 0 y))
        (<= (logand x y) y)))
    (:linear :corollary (implies (and (integerp x) (integerp y) (<= 0 y))
        (<= (logand x y) y)))))

logand-bounds-negtheorem

(defthm logand-bounds-neg
  (implies (and (integerp x) (integerp y) (< x 0) (< y 0))
    (<= (logand x y) x))
  :hints (("Goal" :in-theory (enable logand)))
  :rule-classes ((:rewrite) (:linear)
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (< x 0) (< y 0))
        (<= (logand x y) y)))
    (:linear :corollary (implies (and (integerp x) (integerp y) (< x 0) (< y 0))
        (<= (logand x y) y)))))

|(equal (logand x y) -1)|theorem

(defthm |(equal (logand x y) -1)|
  (equal (equal (logand x y) -1)
    (and (equal x -1) (equal y -1))))

|(< (logand x y) 0)|theorem

(defthm |(< (logand x y) 0)|
  (equal (< (logand x y) 0)
    (and (integerp x) (< x 0) (integerp y) (< y 0)))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (integerp x) (< x 0) (integerp y) (< y 0))
        (and (integerp (logand x y)) (< (logand x y) 0))))
    (:type-prescription :corollary (implies (and (integerp x) (integerp y) (<= 0 y))
        (and (integerp (logand x y)) (<= 0 (logand x y)))))
    (:type-prescription :corollary (implies (and (integerp x) (<= 0 x) (integerp y))
        (and (integerp (logand x y)) (<= 0 (logand x y)))))))

|(logand (* 2 x) (* 2 y))|theorem

(defthm |(logand (* 2 x) (* 2 y))|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (integerp (* 2 x))
      (integerp (* 2 y)))
    (equal (logand (* 2 x) (* 2 y))
      (cond ((and (integerp x) (integerp y)) (* 2 (logand x y)))
        ((and (integerp x) (not (integerp y))) (* 2 (logand x (+ -1/2 y))))
        ((and (not (integerp x)) (integerp y)) (* 2 (logand (+ -1/2 x) y)))
        (t (+ 1 (* 2 (logand (+ -1/2 x) (+ -1/2 y))))))))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (real/rationalp x)
         (real/rationalp y)
         (integerp (* 2 x))
         (integerp (* 2 y)))
       (equal (logand (* 2 x) (* 2 y))
         (cond ((and (integerp x) (integerp y)) (* 2 (logand x y)))
           ((and (integerp x) (not (integerp y))) (* 2 (logand x (+ -1/2 y))))
           ((and (not (integerp x)) (integerp y)) (* 2 (logand (+ -1/2 x) y)))
           (t (+ 1 (* 2 (logand (+ -1/2 x) (+ -1/2 y))))))))) (:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
          (integerp (* 2 x))
          (integerp (* 2 y))
          (integerp x)
          (integerp y))
        (equal (logand (* 2 x) (* 2 y)) (* 2 (logand x y)))))
    (:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
          (integerp (* 2 x))
          (integerp (* 2 y))
          (real/rationalp x)
          (not (integerp x))
          (integerp y))
        (equal (logand (* 2 x) (* 2 y)) (* 2 (logand (+ -1/2 x) y)))))
    (:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
          (integerp (* 2 x))
          (integerp (* 2 y))
          (integerp x)
          (real/rationalp y)
          (not (integerp y)))
        (equal (logand (* 2 x) (* 2 y)) (* 2 (logand x (+ -1/2 y))))))
    (:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
          (integerp (* 2 x))
          (integerp (* 2 y))
          (real/rationalp x)
          (not (integerp x))
          (real/rationalp y)
          (not (integerp y)))
        (equal (logand (* 2 x) (* 2 y))
          (+ 1 (* 2 (logand (+ -1/2 x) (+ -1/2 y)))))))))

|(logand (floor x 2) (floor y 2))|theorem

(defthm |(logand (floor x 2) (floor y 2))|
  (implies (and (integerp x) (integerp y))
    (equal (logand (floor x 2) (floor y 2))
      (floor (logand x y) 2)))
  :rule-classes ((:rewrite :corollary (implies (and (integerp x) (integerp y))
       (equal (logand (floor x 2) (floor y 2))
         (floor (logand x y) 2)))) (:rewrite :corollary (implies (and (integerp x) (integerp y) (integerp (* 1/2 y)))
        (equal (logand (floor x 2) (* 1/2 y))
          (floor (logand x y) 2))))
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (not (integerp (* 1/2 y))))
        (equal (logand (floor x 2) (+ -1/2 (* 1/2 y)))
          (floor (logand x y) 2))))
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (integerp (* 1/2 x)))
        (equal (logand (* 1/2 x) (floor y 2))
          (floor (logand x y) 2))))
    (:rewrite :corollary (implies (and (integerp x)
          (integerp y)
          (integerp (* 1/2 x))
          (integerp (* 1/2 y)))
        (equal (logand (* 1/2 x) (* 1/2 y)) (floor (logand x y) 2))))
    (:rewrite :corollary (implies (and (integerp x)
          (integerp y)
          (integerp (* 1/2 x))
          (not (integerp (* 1/2 y))))
        (equal (logand (* 1/2 x) (+ -1/2 (* 1/2 y)))
          (floor (logand x y) 2))))
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (not (integerp (* 1/2 x))))
        (equal (logand (+ -1/2 (* 1/2 x)) (floor y 2))
          (floor (logand x y) 2))))
    (:rewrite :corollary (implies (and (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (integerp (* 1/2 y)))
        (equal (logand (+ -1/2 (* 1/2 x)) (* 1/2 y))
          (floor (logand x y) 2))))
    (:rewrite :corollary (implies (and (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (not (integerp (* 1/2 y))))
        (equal (logand (+ -1/2 (* 1/2 x)) (+ -1/2 (* 1/2 y)))
          (floor (logand x y) 2))))))

local

(local (defun ind-fn
    (n)
    (cond ((not (integerp n)) 0)
      ((equal n 0) 1)
      ((< n 0) (ind-fn (+ 1 n)))
      (t (ind-fn (+ -1 n))))))

logand-floor-expt-2-nencapsulate

(encapsulate nil
  (local (in-theory (enable expt-type-prescription-integerp-base)))
  (defthm logand-floor-expt-2-n
    (implies (and (integerp x) (integerp y) (integerp n))
      (equal (logand (floor x (expt 2 n)) (floor y (expt 2 n)))
        (floor (logand x y) (expt 2 n))))
    :hints (("Goal" :induct (ind-fn n)
       :do-not '(generalize eliminate-destructors)) ("Subgoal *1/3" :use ((:instance |(logand (floor x 2) (floor y 2))|
           (x (floor x (expt 2 (+ -1 n))))
           (y (floor y (expt 2 (+ -1 n))))))
        :in-theory (disable |(logand (floor x 2) (floor y 2))| logand)))))

|(mod (logand x y) 2)|theorem

(defthm |(mod (logand x y) 2)|
  (implies (and (integerp x) (integerp y))
    (equal (mod (logand x y) 2)
      (if (and (not (integerp (* 1/2 x))) (not (integerp (* 1/2 y))))
        1
        0)))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (integerp x)
         (integerp y))
       (equal (mod (logand x y) 2)
         (if (and (not (integerp (* 1/2 x))) (not (integerp (* 1/2 y))))
           1
           0)))) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (not (integerp (* 1/2 y))))
        (equal (mod (logand x y) 2) 1)))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (integerp (* 1/2 x)))
        (equal (mod (logand x y) 2) 0)))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (integerp (* 1/2 y)))
        (equal (mod (logand x y) 2) 0)))))

mod-logandencapsulate

(encapsulate nil
  (local (defun floor-2-n-ind
      (x y n)
      (cond ((zip n) (+ x y))
        ((< 0 n) (floor-2-n-ind (floor x 2) (floor y 2) (+ -1 n)))
        (t (floor-2-n-ind (floor x 2) (floor y 2) (+ 1 n))))))
  (local (defthm break-logand-apart
      (implies (and (integerp x) (integerp y))
        (equal (logand x y)
          (+ (* 2 (logand (floor x 2) (floor y 2)))
            (logand (mod x 2) (mod y 2)))))
      :hints (("Subgoal 4'" :in-theory (disable logand)))
      :rule-classes nil))
  (local (in-theory (enable expt-type-prescription-integerp-base mod-zero)))
  (local (defthm |(integerp (* 1/2 (mod x (expt 2 n))))|
      (implies (and (< 0 n) (integerp n))
        (equal (integerp (* 1/2 (mod x (expt 2 n))))
          (integerp (* 1/2 x))))))
  (local (in-theory (disable cancel-mod-+
        (:type-prescription mod-zero . 4)
        default-mod-ratio
        default-times-2
        default-+-2
        (:rewrite mod-x-y-=-x-y . 2)
        (:rewrite mod-x-y-=-x . 4))))
  (defthm mod-logand
    (implies (and (integerp x) (integerp y) (integerp n))
      (equal (logand (mod x (expt 2 n)) (mod y (expt 2 n)))
        (mod (logand x y) (expt 2 n))))
    :hints (("Goal" :induct (floor-2-n-ind x y n)
       :in-theory (disable logand)
       :do-not '(generalize eliminate-destructors)) ("Subgoal *1/2" :use ((:instance break-logand-apart) (:instance break-logand-apart
            (x (mod x (expt 2 n)))
            (y (mod y (expt 2 n)))))))))

|(integerp (* 1/2 (logand x y)))|theorem

(defthm |(integerp (* 1/2 (logand x y)))|
  (implies (and (integerp x) (integerp y))
    (equal (integerp (* 1/2 (logand x y)))
      (or (integerp (* 1/2 x)) (integerp (* 1/2 y)))))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (integerp x)
         (integerp y))
       (equal (integerp (* 1/2 (logand x y)))
         (or (integerp (* 1/2 x)) (integerp (* 1/2 y)))))) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (integerp (* 1/2 x)))
        (integerp (* 1/2 (logand x y)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (integerp (* 1/2 y)))
        (integerp (* 1/2 (logand x y)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (not (integerp (* 1/2 y))))
        (not (integerp (* 1/2 (logand x y))))))))

local

(local (defun ind-hint
    (x n)
    (declare (xargs :measure (nfix n)))
    (if (or (zip x) (zp n))
      t
      (ind-hint (floor x 2) (+ -1 n)))))

logand-masktheorem

(defthm logand-mask
  (implies (and (integerp x) (integerp n) (<= 0 n))
    (equal (logand x (+ -1 (expt 2 n))) (mod x (expt 2 n))))
  :hints (("Goal" :do-not '(generalize)
     :in-theory (enable mod)
     :cases ((equal n 0))) ("Subgoal 2" :induct (ind-hint x n))))

l-c-m-fnfunction

(defun l-c-m-fn
  (c)
  (let ((n (power-of-2-minus-1 c)))
    (if n
      (list (cons 'n (kwote n)))
      nil)))

logand-constant-masktheorem

(defthm logand-constant-mask
  (implies (and (bind-free (l-c-m-fn c) (n))
      (integerp n)
      (<= 0 n)
      (equal (+ -1 (expt 2 n)) c)
      (integerp x))
    (equal (logand c x) (mod x (+ 1 c)))))

logand-mask-shiftedencapsulate

(encapsulate nil
  (local (in-theory (enable expt-type-prescription-integerp-base
        default-expt-1
        default-expt-2
        mod-zero)))
  (local (in-theory (disable (:rewrite mod-x-y-=-x-y . 2)
        default-plus-1
        default-plus-2
        default-times-1
        default-times-2
        (:type-prescription mod-zero . 4)
        (:type-prescription floor-zero . 4)
        cancel-mod-+
        (:rewrite mod-x-y-=-x . 3)
        (:rewrite mod-x-y-=-x . 4))))
  (local (defthm lemma
      (implies (and (equal (expt 2 n1) (mod x (* (expt 2 n1) (expt 2 n2))))
          (not (zp n1)))
        (integerp (* 1/2 x)))))
  (local (defthm lemma2
      (implies (and (equal (+ (* 1/2 (expt 2 n1))
              (logand (+ -1/2 (* 1/2 x))
                (+ (* -1/2 (expt 2 n1)) (* 1/2 (expt 2 n1) (expt 2 n2)))))
            (* 1/2 (mod x (* (expt 2 n1) (expt 2 n2)))))
          (not (zp n1)))
        (integerp (* 1/2 x)))))
  (local (defthm lemma3
      (implies (and (equal (+ (* 1/2 (expt 2 n1))
              (logand (+ -1/2 (* 1/2 x))
                (+ (* -1/2 (expt 2 n1)) (* 1/2 (expt 2 n1) (expt 2 n2)))))
            (+ (* 1/2 (expt 2 n1) (expt 2 n2))
              (* 1/2 (mod x (* (expt 2 n1) (expt 2 n2))))))
          (not (zp n1))
          (integerp n2)
          (<= 0 n2))
        (integerp (* 1/2 x)))))
  (defthm logand-mask-shifted
    (implies (and (integerp x)
        (integerp n1)
        (integerp n2)
        (<= 0 n1)
        (<= 0 n2))
      (equal (logand x (* (expt 2 n1) (+ -1 (expt 2 n2))))
        (* (expt 2 n1) (mod (floor x (expt 2 n1)) (expt 2 n2)))))
    :hints (("Goal" :do-not '(generalize) :induct (ind-hint x n1)))))

in-theory

(in-theory (disable logand))

|(logior y x)|theorem

(defthm |(logior y x)| (equal (logior y x) (logior x y)))

|(logior (logior x y) z)|theorem

(defthm |(logior (logior x y) z)|
  (equal (logior (logior x y) z) (logior x y z)))

|(logior y x z)|theorem

(defthm |(logior y x z)|
  (equal (logior y x z) (logior x y z)))

|(logior c d x)|theorem

(defthm |(logior c d x)|
  (implies (and (syntaxp (quotep c)) (syntaxp (quotep d)))
    (equal (logior c d x) (logior (logior c d) x))))

logior-0-xtheorem

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

|(logior 1 x)|theorem

(defthm |(logior 1 x)|
  (implies (integerp x)
    (equal (logior 1 x)
      (if (evenp x)
        (+ 1 x)
        x)))
  :hints (("Goal" :in-theory (enable logand))))

logior--1-xtheorem

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

logior-x-xtheorem

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

logior-bounds-postheorem

(defthm logior-bounds-pos
  (implies (and (integerp x) (integerp y) (<= 0 x) (<= 0 y))
    (<= x (logior x y)))
  :hints (("Goal" :in-theory (e/d (logior lognot) (logand-bounds-neg))
     :use (:instance logand-bounds-neg
       (x (+ -1 (- x)))
       (y (+ -1 (- y))))))
  :rule-classes ((:rewrite) (:linear)
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (<= 0 x) (<= 0 y))
        (<= y (logior x y))))
    (:linear :corollary (implies (and (integerp x) (integerp y) (<= 0 x) (<= 0 y))
        (<= y (logior x y))))))

logior-bounds-negtheorem

(defthm logior-bounds-neg
  (implies (and (integerp x) (integerp y) (< 0 x) (< 0 y))
    (<= x (logior x y)))
  :hints (("Goal" :in-theory (e/d (logior lognot) (logand-bounds-neg))
     :use (:instance logand-bounds-neg
       (x (+ -1 (- x)))
       (y (+ -1 (- y))))))
  :rule-classes ((:rewrite) (:linear)
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (< x 0) (< y 0))
        (<= y (logior x y))))
    (:linear :corollary (implies (and (integerp x) (integerp y) (< x 0) (< y 0))
        (<= y (logior x y))))))

|(equal (logior x y) 0)|theorem

(defthm |(equal (logior x y) 0)|
  (implies (and (integerp x) (integerp y))
    (equal (equal (logior x y) 0) (and (equal x 0) (equal y 0)))))

|(< (logior x y) 0)|theorem

(defthm |(< (logior x y) 0)|
  (implies (and (integerp x) (integerp y))
    (equal (< (logior x y) 0) (or (< x 0) (< y 0))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (integerp x) (integerp y) (< x 0))
        (< (logior x y) 0)))
    (:type-prescription :corollary (implies (and (integerp x) (integerp y) (< y 0))
        (< (logior x y) 0)))))

|(< 0 (logior x y))|theorem

(defthm |(< 0 (logior x y))|
  (implies (and (integerp x) (integerp y))
    (equal (< 0 (logior x y))
      (or (and (< 0 x) (<= 0 y)) (and (<= 0 x) (< 0 y)))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (integerp x) (integerp y) (< 0 x) (<= 0 y))
        (< 0 (logior x y))))
    (:type-prescription :corollary (implies (and (integerp x) (integerp y) (<= 0 x) (< 0 y))
        (< 0 (logior x y))))))

|(logior (* 2 x) (* 2 y))|theorem

(defthm |(logior (* 2 x) (* 2 y))|
  (implies (and (real/rationalp x)
      (real/rationalp y)
      (integerp (* 2 x))
      (integerp (* 2 y)))
    (equal (logior (* 2 x) (* 2 y))
      (cond ((and (integerp x) (integerp y)) (* 2 (logior x y)))
        ((and (integerp x) (not (integerp y))) (+ 1 (* 2 (logior x (+ -1/2 y)))))
        ((and (not (integerp x)) (integerp y)) (+ 1 (* 2 (logior (+ -1/2 x) y))))
        (t (+ 1 (* 2 (logior (+ -1/2 x) (+ -1/2 y))))))))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (real/rationalp x)
         (real/rationalp y)
         (integerp (* 2 x))
         (integerp (* 2 y)))
       (equal (logior (* 2 x) (* 2 y))
         (cond ((and (integerp x) (integerp y)) (* 2 (logior x y)))
           ((and (integerp x) (not (integerp y))) (+ 1 (* 2 (logior x (+ -1/2 y)))))
           ((and (not (integerp x)) (integerp y)) (+ 1 (* 2 (logior (+ -1/2 x) y))))
           (t (+ 1 (* 2 (logior (+ -1/2 x) (+ -1/2 y))))))))) (:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
          (integerp (* 2 x))
          (integerp (* 2 y))
          (integerp x)
          (integerp y))
        (equal (logior (* 2 x) (* 2 y)) (* 2 (logior x y)))))
    (:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
          (integerp (* 2 x))
          (integerp (* 2 y))
          (real/rationalp x)
          (not (integerp x))
          (integerp y))
        (equal (logior (* 2 x) (* 2 y))
          (+ 1 (* 2 (logior (+ -1/2 x) y))))))
    (:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
          (integerp (* 2 x))
          (integerp (* 2 y))
          (integerp x)
          (real/rationalp y)
          (not (integerp y)))
        (equal (logior (* 2 x) (* 2 y))
          (+ 1 (* 2 (logior x (+ -1/2 y)))))))
    (:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
          (integerp (* 2 x))
          (integerp (* 2 y))
          (real/rationalp x)
          (not (integerp x))
          (real/rationalp y)
          (not (integerp y)))
        (equal (logior (* 2 x) (* 2 y))
          (+ 1 (* 2 (logior (+ -1/2 x) (+ -1/2 y))))))))
  :hints (("Goal" :expand ((logand (+ -1 (* -2 x)) (+ -1 (* -2 y)))))))

|(logior (floor x 2) (floor y 2))|theorem

(defthm |(logior (floor x 2) (floor y 2))|
  (implies (and (integerp x) (integerp y))
    (equal (logior (floor x 2) (floor y 2))
      (floor (logior x y) 2)))
  :rule-classes ((:rewrite :corollary (implies (and (integerp x) (integerp y))
       (equal (logior (floor x 2) (floor y 2))
         (floor (logior x y) 2)))) (:rewrite :corollary (implies (and (integerp x) (integerp y) (integerp (* 1/2 y)))
        (equal (logior (floor x 2) (* 1/2 y))
          (floor (logior x y) 2))))
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (not (integerp (* 1/2 y))))
        (equal (logior (floor x 2) (+ -1/2 (* 1/2 y)))
          (floor (logior x y) 2))))
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (integerp (* 1/2 x)))
        (equal (logior (* 1/2 x) (floor y 2))
          (floor (logior x y) 2))))
    (:rewrite :corollary (implies (and (integerp x)
          (integerp y)
          (integerp (* 1/2 x))
          (integerp (* 1/2 y)))
        (equal (logior (* 1/2 x) (* 1/2 y)) (floor (logior x y) 2))))
    (:rewrite :corollary (implies (and (integerp x)
          (integerp y)
          (integerp (* 1/2 x))
          (not (integerp (* 1/2 y))))
        (equal (logior (* 1/2 x) (+ -1/2 (* 1/2 y)))
          (floor (logior x y) 2))))
    (:rewrite :corollary (implies (and (integerp x) (integerp y) (not (integerp (* 1/2 x))))
        (equal (logior (+ -1/2 (* 1/2 x)) (floor y 2))
          (floor (logior x y) 2))))
    (:rewrite :corollary (implies (and (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (integerp (* 1/2 y)))
        (equal (logior (+ -1/2 (* 1/2 x)) (* 1/2 y))
          (floor (logior x y) 2))))
    (:rewrite :corollary (implies (and (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (not (integerp (* 1/2 y))))
        (equal (logior (+ -1/2 (* 1/2 x)) (+ -1/2 (* 1/2 y)))
          (floor (logior x y) 2)))))
  :hints (("Goal" :in-theory (enable logand))))

logior-floor-expt-2-ntheorem

(defthm logior-floor-expt-2-n
  (implies (and (integerp x) (integerp y) (integerp n) (<= 0 n))
    (equal (logior (floor x (expt 2 n)) (floor y (expt 2 n)))
      (floor (logior x y) (expt 2 n))))
  :hints (("Goal" :in-theory (e/d nil (logior))
     :induct (ind-fn n)
     :do-not '(generalize eliminate-destructors)) ("Subgoal *1/2" :use ((:instance |(logior (floor x 2) (floor y 2))|
         (x (floor x (expt 2 (+ -1 n))))
         (y (floor y (expt 2 (+ -1 n)))))))))

|(mod (logior x y) 2)|theorem

(defthm |(mod (logior x y) 2)|
  (implies (and (integerp x) (integerp y))
    (equal (mod (logior x y) 2)
      (if (and (integerp (* 1/2 x)) (integerp (* 1/2 y)))
        0
        1)))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (integerp x)
         (integerp y))
       (equal (mod (logior x y) 2)
         (if (and (integerp (* 1/2 x)) (integerp (* 1/2 y)))
           0
           1)))) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (integerp (* 1/2 x))
          (integerp (* 1/2 y)))
        (equal (mod (logior x y) 2) 0)))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x))))
        (equal (mod (logior x y) 2) 1)))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (not (integerp (* 1/2 y))))
        (equal (mod (logior x y) 2) 1)))))

mod-logior-expt-2-nencapsulate

(encapsulate nil
  (local (in-theory (enable expt-type-prescription-integerp-base mod-zero)))
  (local (defun floor-2-n-ind
      (x y n)
      (cond ((zip n) (+ x y))
        ((< 0 n) (floor-2-n-ind (floor x 2) (floor y 2) (+ -1 n)))
        (t (floor-2-n-ind (floor x 2) (floor y 2) (+ 1 n))))))
  (local (defthm |(integerp (* 1/2 (logior x y)))|
      (implies (and (integerp x) (integerp y))
        (equal (integerp (* 1/2 (logior x y)))
          (and (integerp (* 1/2 x)) (integerp (* 1/2 y)))))))
  (local (defthm break-logior-apart
      (implies (and (integerp x) (integerp y))
        (equal (logior x y)
          (+ (* 2 (logior (floor x 2) (floor y 2)))
            (logior (mod x 2) (mod y 2)))))
      :hints (("Goal" :in-theory (disable logior)))
      :rule-classes nil))
  (local (defthm crock-0
      (implies (and (integerp x)
          (not (integerp (* 1/2 x)))
          (integerp n)
          (< 0 n))
        (not (integerp (* 1/2 (mod x (expt 2 n))))))))
  (local (defthm crock-1
      (implies (and (integerp x) (integerp (* 1/2 x)) (integerp n) (< 0 n))
        (integerp (* 1/2 (mod x (expt 2 n)))))))
  (local (defthm crock-2
      (implies (and (equal (mod x (expt 2 n)) 0)
          (integerp x)
          (integerp n)
          (< 0 n))
        (integerp (* 1/2 x)))))
  (local (in-theory (disable (:type-prescription not-integerp-4a)
        (:type-prescription mod-zero . 4)
        (:type-prescription not-integerp-4b)
        (:rewrite mod-x-y-=-x-y . 2)
        (:type-prescription mod-zero . 2)
        (:rewrite cancel-mod-+)
        (:rewrite default-times-2)
        (:type-prescription expt-type-prescription-nonpositive-base-odd-exponent)
        (:type-prescription expt-type-prescription-nonpositive-base-even-exponent)
        (:type-prescription expt-type-prescription-negative-base-odd-exponent)
        (:type-prescription expt-type-prescription-negative-base-even-exponent)
        (:type-prescription expt-type-prescription-integerp-base-b)
        (:rewrite default-plus-2)
        (:rewrite default-mod-ratio)
        (:type-prescription not-integerp-3b)
        (:type-prescription not-integerp-2b)
        (:type-prescription not-integerp-1b)
        (:type-prescription integerp-/-expt-2)
        (:rewrite mod-x-y-=-x-y . 1)
        (:rewrite mod-x-y-=-x . 4)
        (:rewrite simplify-products-gather-exponents-<)
        (:rewrite mod-x-y-=-x+y . 1)
        (:type-prescription |(< (logior x y) 0)| . 2)
        (:type-prescription |(< (logior x y) 0)| . 1)
        (:rewrite default-plus-1)
        (:rewrite default-times-1)
        (:rewrite |(mod (+ x (mod a b)) y)|)
        (:rewrite |(mod (+ x (- (mod a b))) y)|)
        (:rewrite default-divide)
        (:type-prescription mod-zero . 3)
        (:type-prescription mod-positive . 2)
        (:type-prescription mod-positive . 1)
        (:type-prescription mod-negative . 2)
        (:type-prescription mod-negative . 1)
        (:rewrite mod-x-y-=-x-y . 3)
        (:rewrite simplify-products-gather-exponents-equal)
        (:type-prescription mod-nonpositive)
        (:type-prescription not-integerp-3a)
        (:type-prescription not-integerp-2a)
        (:rewrite |(* (- x) y)|)
        (:rewrite mod-x-y-=-x . 2)
        (:rewrite |(< (logior x y) 0)|)
        (:rewrite default-minus)
        (:rewrite default-less-than-2)
        (:rewrite default-less-than-1)
        (:rewrite mod-cancel-*-const)
        (:type-prescription not-integerp-1a)
        (:rewrite mod-x-y-=-x+y . 3)
        (:type-prescription not-integerp-4a)
        (:rewrite default-times-2)
        (:rewrite |(mod x (* y (/ z))) rewriting-goal-literal|)
        (:type-prescription not-integerp-4b-expt)
        (:rewrite default-mod-2)
        (:rewrite reduce-additive-constant-<)
        (:type-prescription not-integerp-3b-expt)
        (:rewrite |(* (+ x y) z)|)
        (:type-prescription not-integerp-4a-expt)
        (:linear mod-bounds-2)
        (:type-prescription not-integerp-2b-expt)
        (:rewrite default-expt-2)
        (:rewrite default-expt-1)
        (:type-prescription bubble-down)
        (:rewrite default-floor-ratio)
        (:rewrite reduce-rational-multiplicative-constant-<)
        (:rewrite reduce-multiplicative-constant-<)
        (:rewrite the-floor-below)
        (:rewrite the-floor-above)
        (:rewrite integerp-<-constant)
        (:rewrite remove-strict-inequalities)
        (:rewrite |(< (/ x) (/ y))|)
        (:rewrite |(< c (/ x)) positive c --- present in goal|)
        (:rewrite |(< c (/ x)) positive c --- obj t or nil|)
        (:rewrite |(< c (/ x)) negative c --- present in goal|)
        (:rewrite |(< c (/ x)) negative c --- obj t or nil|)
        (:rewrite |(< (/ x) c) positive c --- present in goal|)
        (:rewrite |(< (/ x) c) positive c --- obj t or nil|)
        (:rewrite |(< (/ x) c) negative c --- present in goal|)
        (:rewrite |(< (/ x) c) negative c --- obj t or nil|)
        (:rewrite constant-<-integerp)
        (:rewrite |(* (if a b c) x)|)
        (:rewrite |(< (+ (- c) x) y)|)
        (:type-prescription integerp-mod-2)
        (:type-prescription integerp-mod-1)
        (:type-prescription rationalp-mod)
        (:rewrite normalize-terms-such-as-a/a+b-+-b/a+b)
        (:meta meta-integerp-correct)
        (:rewrite reduce-additive-constant-equal)
        (:linear expt-x->-x)
        (:rewrite default-mod-1)
        (:linear expt-x->=-x)
        (:type-prescription floor-zero . 4)
        (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-remainder)
        (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-common)
        (:linear expt-<=-1-two)
        (:rewrite |(< (* x y) 0)|)
        (:rewrite |(< (/ x) 0)|)
        (:linear expt-is-weakly-increasing-for-base->-1)
        (:rewrite |(equal (- x) (- y))|)
        (:linear expt-linear-upper-<=)
        (:rewrite reduce-multiplicative-constant-equal)
        (:rewrite |(equal (/ x) c)|)
        (:rewrite |(equal (- x) c)|)
        (:type-prescription not-integerp-3a-expt)
        (:type-prescription not-integerp-2a-expt)
        (:type-prescription not-integerp-1a-expt)
        (:linear expt-is-weakly-decreasing-for-pos-base-<-1)
        (:linear expt-is-decreasing-for-pos-base-<-1)
        (:rewrite |(equal c (/ x))|)
        (:rewrite |(equal (/ x) (/ y))|)
        (:rewrite equal-of-predicates-rewrite)
        (:rewrite |(equal c (- x))|)
        (:type-prescription floor-zero . 2)
        (:rewrite |(< x (+ c/d y))|)
        (:rewrite default-floor-1)
        (:linear expt-<-1-two)
        (:type-prescription floor-nonpositive . 1)
        (:type-prescription floor-positive . 1)
        (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-remainder)
        (:rewrite simplify-terms-such-as-0-<-ax+bx-rational-common)
        (:rewrite |(< 0 (* x y))|)
        (:rewrite simplify-terms-such-as-ax+bx-=-0)
        (:rewrite mod-zero . 1)
        (:linear expt-linear-upper-<)
        (:linear expt-linear-lower-<)
        (:linear expt->=-1-two)
        (:linear expt->-1-two)
        (:linear expt-<=-1-one)
        (:linear expt-<-1-one)
        (:rewrite mod-cancel-*-not-rewriting-goal-literal)
        (:rewrite |(mod x (- y))| . 3)
        (:rewrite |(mod x (- y))| . 2)
        (:rewrite |(mod x (* y (/ z))) not rewriting-goal-literal|)
        (:rewrite |(mod (- x) y)| . 3)
        (:rewrite |(mod (- x) y)| . 2)
        (:rewrite |(mod (- x) y)| . 1)
        (:rewrite |(mod (* x (/ y)) z) not rewriting-goal-literal|)
        (:rewrite |(equal (mod (+ x y) z) x)|)
        (:type-prescription abs)
        (:rewrite simplify-products-scatter-exponents-<)
        (:rewrite |(not (equal x (/ y)))|)
        (:rewrite prefer-positive-exponents-scatter-exponents-<)
        (:type-prescription floor-zero . 3)
        (:type-prescription floor-zero . 1)
        (:type-prescription floor-positive . 3)
        (:type-prescription floor-positive . 2)
        (:type-prescription floor-nonpositive . 3)
        (:type-prescription floor-nonpositive . 2)
        (:type-prescription floor-nonnegative . 3)
        (:type-prescription floor-nonnegative . 2)
        (:type-prescription floor-negative . 3)
        (:type-prescription floor-negative . 2)
        (:type-prescription floor-negative . 1)
        (:type-prescription floor-nonnegative . 1)
        (:rewrite |(equal x (/ y))|)
        (:rewrite mod-zero . 2))))
  (defthm mod-logior-expt-2-n
    (implies (and (integerp x) (integerp y) (integerp n))
      (equal (logior (mod x (expt 2 n)) (mod y (expt 2 n)))
        (mod (logior x y) (expt 2 n))))
    :hints (("Goal" :induct (floor-2-n-ind x y n)
       :in-theory (disable logior)
       :do-not '(generalize eliminate-destructors)) ("Subgoal *1/2" :use ((:instance break-logior-apart) (:instance break-logior-apart
            (x (mod x (expt 2 n)))
            (y (mod y (expt 2 n)))))))))

|(integerp (* 1/2 (logior x y)))|theorem

(defthm |(integerp (* 1/2 (logior x y)))|
  (implies (and (integerp x) (integerp y))
    (equal (integerp (* 1/2 (logior x y)))
      (and (integerp (* 1/2 x)) (integerp (* 1/2 y))))))

in-theory

(in-theory (disable logior))

|(logxor y x)|theorem

(defthm |(logxor y x)| (equal (logxor y x) (logxor x y)))

logxor-0-xtheorem

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

logxor-1-xtheorem

(defthm logxor-1-x
  (implies (integerp x)
    (equal (logxor 1 x)
      (if (evenp x)
        (+ 1 x)
        (+ -1 x))))
  :hints (("Goal" :in-theory (enable logior logand))))

logxor--1-xtheorem

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

logxor-x-xtheorem

(defthm logxor-x-x
  (implies (integerp x) (equal (logxor x x) 0))
  :hints (("Goal" :in-theory (enable logior logand))))

|(logxor (floor x 2) (floor y 2))|encapsulate

(encapsulate nil
  (local (in-theory (e/d nil
        (reduce-additive-constant-< (:rewrite |(< (- x) c)|)
          (:type-prescription |(< (logand x y) 0)| . 3)
          (:type-prescription |(< (logand x y) 0)| . 2)
          (:type-prescription |(< (logand x y) 0)| . 1)
          (:linear logand-bounds-pos . 1)
          (:linear logand-bounds-pos . 2)
          (:linear logand-bounds-neg . 2)
          (:linear logand-bounds-neg . 1)
          (:rewrite prefer-positive-addends-equal)
          (:rewrite normalize-addends)
          (:rewrite |(< (+ (- c) x) y)|)
          (:rewrite |(< x (/ y)) with (< 0 y)|)
          (:rewrite |(<= 1 (* (/ x) y)) with (< x 0)|)
          (:rewrite |(<= (* (/ x) y) -1) with (< 0 x)|)
          (:rewrite |(<= 1 (* (/ x) y)) with (< 0 x)|)
          (:rewrite |(<= (* (/ x) y) -1) with (< x 0)|)
          (:rewrite |(< (/ x) y) with (< 0 x)|)
          (:rewrite |(<= (/ x) y) with (< 0 x)|)
          (:rewrite |(< (* (/ x) y) 1) with (< x 0)|)
          (:rewrite |(floor (* x (/ y)) z) not rewriting-goal-literal|)
          (:rewrite |(< -1 (* (/ x) y)) with (< 0 x)|)
          (:rewrite |(< x (/ y)) with (< y 0)|)
          (:rewrite |(<= (/ x) y) with (< x 0)|)
          (:rewrite |(< -1 (* (/ x) y)) with (< x 0)|)
          (:rewrite |(< (* (/ x) y) 1) with (< 0 x)|)
          (:rewrite reduce-multiplicative-constant-<)
          (:rewrite |(< (+ c/d x) y)|)
          (:rewrite normalize-terms-such-as-a/a+b-+-b/a+b)
          (:rewrite default-less-than-2)
          (:rewrite |(floor (+ x y) z) where (< 0 z)| . 3)
          (:rewrite prefer-positive-addends-<)
          (:rewrite |(floor (+ x y) z) where (< 0 z)| . 2)
          (:rewrite normalize-factors-gather-exponents)
          (:rewrite the-floor-above)
          (:rewrite floor-x-y-=--1 . 2)
          (:rewrite reduce-rational-multiplicative-constant-<)
          (:rewrite |(* (- x) y)|)
          (:rewrite |(< (- x) (- y))|)
          (:rewrite |(< (* x y) 0)|)
          (:rewrite constant-<-integerp)
          (:rewrite simplify-products-gather-exponents-<)
          (:rewrite |(floor x 2)| . 2)
          (:rewrite |(< (logior x y) 0)|)
          (:rewrite floor-=-x/y . 1)
          (:rewrite |(< c (/ x)) positive c --- present in goal|)
          (:rewrite |(< c (/ x)) positive c --- obj t or nil|)
          (:rewrite |(< c (/ x)) negative c --- present in goal|)
          (:rewrite |(< c (/ x)) negative c --- obj t or nil|)
          (:rewrite |(< c (- x))|)
          (:rewrite |(< (/ x) c) positive c --- present in goal|)
          (:rewrite |(< (/ x) c) positive c --- obj t or nil|)
          (:rewrite |(< (/ x) c) negative c --- present in goal|)
          (:rewrite |(< (/ x) c) negative c --- obj t or nil|)
          (:rewrite |(< (/ x) (/ y))|)
          (:rewrite mod-cancel-*-const)
          (:rewrite remove-strict-inequalities)
          (:rewrite integerp-<-constant)
          (:rewrite floor-cancel-*-const)
          (:rewrite mod-x-y-=-x+y . 2)
          (:rewrite simplify-sums-<)
          (:rewrite reduce-integerp-+)
          (:meta meta-integerp-correct)
          (:linear logior-bounds-pos . 2)
          (:linear logior-bounds-pos . 1)
          (:linear logior-bounds-neg . 2)
          (:linear logior-bounds-neg . 1)
          (:rewrite |(* (* x y) z)|)
          (:rewrite simplify-products-gather-exponents-equal)
          (:linear mod-bounds-3)
          (:rewrite mod-x-y-=-x+y . 3)
          (:rewrite default-logand-2)
          (:rewrite remove-weak-inequalities)
          (:rewrite |(< (logand x y) 0)|)
          (:rewrite |(< (/ x) y) with (< x 0)|)
          (:rewrite |(< (/ x) 0)|)
          (:type-prescription |(< 0 (logior x y))| . 2)
          (:type-prescription |(< 0 (logior x y))| . 1)
          (:type-prescription |(< (logior x y) 0)| . 2)
          (:type-prescription |(< (logior x y) 0)| . 1)
          (:rewrite simplify-sums-equal)
          (:rewrite cancel-mod-+)
          (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-remainder)
          (:rewrite simplify-terms-such-as-ax+bx-<-0-rational-common)
          (:rewrite |(equal (/ x) (/ y))|)
          (:rewrite |(equal c (/ x))|)
          (:rewrite |(equal (/ x) c)|)
          (:type-prescription mod-nonnegative)
          (:type-prescription integerp-mod-2)
          (:type-prescription integerp-mod-1)
          (:rewrite |(< (* x y) 0) rationalp (* x y)|)
          (:rewrite default-mod-ratio)
          (:type-prescription rationalp-mod)
          (:rewrite |(floor x (- y))| . 2)
          (:rewrite |(floor (- x) y)| . 2)
          (:rewrite equal-of-predicates-rewrite)
          (:rewrite default-logand-1)
          (:rewrite |(equal (+ (- c) x) y)|)
          (:rewrite |(<= x (/ y)) with (< y 0)|)
          (:rewrite logand-constant-mask)
          (:rewrite |(not (equal (* (/ x) y) -1))|)
          (:rewrite |(equal (* (/ x) y) -1)|)
          (:rewrite |(mod x 2)| . 2)
          (:rewrite |(< x (+ c/d y))|)
          (:rewrite |(< y (+ (- c) x))|)
          (:rewrite default-logior-2)))))
  (defthm |(logxor (floor x 2) (floor y 2))|
    (implies (and (integerp x) (integerp y))
      (equal (logxor (floor x 2) (floor y 2))
        (floor (logxor x y) 2)))
    :rule-classes ((:rewrite :corollary (implies (and (integerp x) (integerp y))
         (equal (logxor (floor x 2) (floor y 2))
           (floor (logxor x y) 2)))) (:rewrite :corollary (implies (and (integerp x) (integerp y) (integerp (* 1/2 y)))
          (equal (logxor (floor x 2) (* 1/2 y))
            (floor (logxor x y) 2))))
      (:rewrite :corollary (implies (and (integerp x) (integerp y) (not (integerp (* 1/2 y))))
          (equal (logxor (floor x 2) (+ -1/2 (* 1/2 y)))
            (floor (logxor x y) 2))))
      (:rewrite :corollary (implies (and (integerp x) (integerp y) (integerp (* 1/2 x)))
          (equal (logxor (* 1/2 x) (floor y 2))
            (floor (logxor x y) 2))))
      (:rewrite :corollary (implies (and (integerp x)
            (integerp y)
            (integerp (* 1/2 x))
            (integerp (* 1/2 y)))
          (equal (logxor (* 1/2 x) (* 1/2 y)) (floor (logxor x y) 2))))
      (:rewrite :corollary (implies (and (integerp x)
            (integerp y)
            (integerp (* 1/2 x))
            (not (integerp (* 1/2 y))))
          (equal (logxor (* 1/2 x) (+ -1/2 (* 1/2 y)))
            (floor (logxor x y) 2))))
      (:rewrite :corollary (implies (and (integerp x) (integerp y) (not (integerp (* 1/2 x))))
          (equal (logxor (+ -1/2 (* 1/2 x)) (floor y 2))
            (floor (logxor x y) 2))))
      (:rewrite :corollary (implies (and (integerp x)
            (integerp y)
            (not (integerp (* 1/2 x)))
            (integerp (* 1/2 y)))
          (equal (logxor (+ -1/2 (* 1/2 x)) (* 1/2 y))
            (floor (logxor x y) 2))))
      (:rewrite :corollary (implies (and (integerp x)
            (integerp y)
            (not (integerp (* 1/2 x)))
            (not (integerp (* 1/2 y))))
          (equal (logxor (+ -1/2 (* 1/2 x)) (+ -1/2 (* 1/2 y)))
            (floor (logxor x y) 2)))))
    :hints (("Goal" :in-theory (enable logior logand)))))

|(mod (logxor x y) 2)|theorem

(defthm |(mod (logxor x y) 2)|
  (implies (and (integerp x) (integerp y))
    (equal (mod (logxor x y) 2)
      (cond ((and (integerp (* 1/2 x)) (not (integerp (* 1/2 y)))) 1)
        ((and (not (integerp (* 1/2 x))) (integerp (* 1/2 y))) 1)
        (t 0))))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (integerp x)
         (integerp y))
       (equal (mod (logxor x y) 2)
         (cond ((and (integerp (* 1/2 x)) (not (integerp (* 1/2 y)))) 1)
           ((and (not (integerp (* 1/2 x))) (integerp (* 1/2 y))) 1)
           (t 0))))) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (integerp (* 1/2 x))
          (not (integerp (* 1/2 y))))
        (equal (mod (logxor x y) 2) 1)))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (integerp (* 1/2 y)))
        (equal (mod (logxor x y) 2) 1)))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (integerp (* 1/2 x))
          (integerp (* 1/2 y)))
        (equal (mod (logxor x y) 2) 0)))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (not (integerp (* 1/2 y))))
        (equal (mod (logxor x y) 2) 0)))))

|(integerp (* 1/2 (logxor x y)))|theorem

(defthm |(integerp (* 1/2 (logxor x y)))|
  (implies (and (integerp x) (integerp y))
    (equal (integerp (* 1/2 (logxor x y)))
      (iff (integerp (* 1/2 x)) (integerp (* 1/2 y)))))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (integerp x)
         (integerp y))
       (equal (integerp (* 1/2 (logxor x y)))
         (iff (integerp (* 1/2 x)) (integerp (* 1/2 y)))))) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (integerp (* 1/2 x))
          (integerp (* 1/2 y)))
        (integerp (* 1/2 (logxor x y)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (not (integerp (* 1/2 y))))
        (integerp (* 1/2 (logxor x y)))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (integerp (* 1/2 x))
          (not (integerp (* 1/2 y))))
        (not (integerp (* 1/2 (logxor x y))))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp y)
          (not (integerp (* 1/2 x)))
          (integerp (* 1/2 y)))
        (not (integerp (* 1/2 (logxor x y))))))))

in-theory

(in-theory (disable logxor))

|(equal (lognot x) (lognot y))|theorem

(defthm |(equal (lognot x) (lognot y))|
  (implies (and (integerp x) (integerp y))
    (equal (equal (lognot x) (lognot y)) (equal x y))))

|(equal (lognot x) -1)|theorem

(defthm |(equal (lognot x) -1)|
  (implies (integerp x)
    (equal (equal (lognot x) -1) (equal x 0))))

|(equal (lognot x) 0)|theorem

(defthm |(equal (lognot x) 0)|
  (equal (equal (lognot x) 0) (equal x -1)))

|(lognot (* 2 x))|theorem

(defthm |(lognot (* 2 x))|
  (implies (and (real/rationalp x) (integerp (* 2 x)))
    (equal (lognot (* 2 x))
      (if (integerp x)
        (+ 1 (* 2 (lognot x)))
        (* 2 (lognot (+ -1/2 x))))))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (real/rationalp x)
         (integerp (* 2 x)))
       (equal (lognot (* 2 x))
         (if (integerp x)
           (+ 1 (* 2 (lognot x)))
           (* 2 (lognot (+ -1/2 x))))))) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x))
        (equal (lognot (* 2 x)) (+ 1 (* 2 (lognot x))))))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp (* 2 x))
          (real/rationalp x)
          (not (integerp x)))
        (equal (lognot (* 2 x)) (* 2 (lognot (+ -1/2 x))))))))

|(lognot (floor x 2))|theorem

(defthm |(lognot (floor x 2))|
  (implies (integerp x)
    (equal (lognot (floor x 2)) (floor (lognot x) 2)))
  :rule-classes ((:rewrite :corollary (implies (integerp x)
       (equal (lognot (floor x 2)) (floor (lognot x) 2)))) (:rewrite :corollary (implies (and (integerp x) (integerp (* 1/2 x)))
        (equal (lognot (* 1/2 x)) (floor (lognot x) 2))))
    (:rewrite :corollary (implies (and (integerp x) (not (integerp (* 1/2 x))))
        (equal (lognot (+ -1/2 (* 1/2 x))) (floor (lognot x) 2))))))

local

(local (defthm floor-lognot-helper
    (implies (and (integerp x) (integerp n) (equal (+ 1 (mod x n)) n))
      (integerp (+ (/ n) (* x (/ n)))))
    :rule-classes nil))

floor-lognotencapsulate

(encapsulate nil
  (local (in-theory (enable expt-type-prescription-integerp-base)))
  (defthm floor-lognot
    (implies (and (integerp x) (integerp n) (<= 0 n))
      (equal (lognot (floor x (expt 2 n)))
        (floor (lognot x) (expt 2 n))))
    :hints (("Goal" :induct (ind-fn n)
       :do-not '(generalize eliminate-destructors)) ("Subgoal *1/2" :use ((:instance (:theorem (implies (equal x y) (equal (floor x 2) (floor y 2))))
           (x (floor (lognot x) (expt 2 (+ -1 n))))
           (y (lognot (floor x (expt 2 (+ -1 n))))))))
      ("Subgoal *1/2.2" :use (:instance floor-lognot-helper (x x) (n (expt 2 n)))))))

|(mod (lognot x) 2)|theorem

(defthm |(mod (lognot x) 2)|
  (implies (integerp x)
    (equal (mod (lognot x) 2)
      (if (integerp (* 1/2 x))
        1
        0)))
  :rule-classes ((:rewrite :corollary (implies (and (syntaxp (rewriting-goal-literal x mfc state))
         (integerp x))
       (equal (mod (lognot x) 2)
         (if (integerp (* 1/2 x))
           1
           0)))) (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (integerp (* 1/2 x)))
        (equal (mod (lognot x) 2) 1)))
    (:rewrite :corollary (implies (and (syntaxp (not (rewriting-goal-literal x mfc state)))
          (integerp x)
          (not (integerp (* 1/2 x))))
        (equal (mod (lognot x) 2) 0)))))

|(integerp (* 1/2 (lognot x)))|theorem

(defthm |(integerp (* 1/2 (lognot x)))|
  (implies (integerp x)
    (equal (integerp (* 1/2 (lognot x)))
      (not (integerp (* 1/2 x))))))

lognot-logandtheorem

(defthm lognot-logand
  (implies (and (integerp x) (integerp y))
    (equal (lognot (logand x y)) (logior (lognot x) (lognot y))))
  :hints (("Goal" :in-theory (enable logior))))

lognot-logiortheorem

(defthm lognot-logior
  (implies (and (integerp x) (integerp y))
    (equal (lognot (logior x y)) (logand (lognot x) (lognot y))))
  :hints (("Goal" :in-theory (enable logior))))

lognot-lognottheorem

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

in-theory

(in-theory (disable lognot))