;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; b-ops-aux.lisp:
;;  This file contains auxiliary lemmas to assist the IHS library
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(in-package "ACL2")

;; [Jared] changed this book to just be an include of the identical book
(include-book "workshops/1999/pipeline/b-ops-aux" :dir :system)

;; (include-book "b-ops-aux-def")

;; (deflabel begin-b-ops-aux)

;; ;; Type of b-if
;; (defthm bitp-b-if
;;     (implies (and (bitp y) (bitp z))
;; 	     (bitp (b-if x y z)))
;;   :hints (("goal" :in-theory (enable bitp))))

;; (defthm integerp-b-if
;;     (implies (and (integerp y) (integerp z))
;; 	     (integerp (b-if x y z)))
;;   :hints (("goal" :in-theory (enable bitp))))

;; (defthm b-not-b-not
;;     (equal (b-not (b-not i)) (bfix i))
;;   :hints (("goal" :in-theory (enable b-not bfix zbp))))

;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;; Here are several basic lemmas about bit operations.

;; ;; If bit vector X is longer than (p+s), bits between the p'th and (p+s)'th
;; ;; bits of the concatenation of x and y is equal to that of x.
;; (defthm rdb-logapp-1
;;     (implies (and (integerp x) (integerp y) (integerp i) (<= 0 i)
;; 		  (integerp s) (<= 0 s) (integerp p) (<= 0 p)
;; 		  (<= (+ s p) i))
;; 	     (equal (rdb (cons s p) (logapp i x y))
;; 		    (rdb (cons s p) x)))
;;   :hints (("Goal" :in-theory (enable logapp* rdb bsp-size bsp-position))))

;; ;; If bit vector X is shorter than p, bits from the p'th LSB to (p+s)'th
;; ;; LSB of the concatenation of x and y is equal to that of y.
;; (defthm rdb-logapp-2
;;     (implies (and (integerp x) (integerp y)
;; 		  (integerp s) (<= 0 s) (integerp p) (<= 0 p)
;; 		  (integerp i) (<= 0 i)
;; 		  (<= i p))
;; 	     (equal (rdb (cons s p) (logapp i x y))
;; 		    (rdb (cons s (- p i)) y)))
;;   :hints (("Goal" :in-theory (enable logapp* rdb bsp-size bsp-position))))


;; (defthm loghead-0
;;     (equal (loghead x 0) 0)
;;   :hints (("Goal" :in-theory (enable loghead))))

;; (defthm loghead-1
;;     (equal (loghead 1 vector) (logcar vector))
;;   :hints (("Goal" :in-theory (enable logcar loghead))))

;; (defthm logcar-bitp
;;     (implies (bitp x)
;; 	     (equal (logcar x) x))
;;   :hints (("Goal" :in-theory (enable bitp logcar))))

;; (defthm logbit-0-bitp
;;     (implies (bitp x)
;; 	     (equal (logbit 0 x) x))
;;     :hints (("Goal" :in-theory (enable bitp logbit))))

;; (defthm loghead-bitp
;;     (implies (bitp x)
;; 	     (equal (loghead 1 x) x))
;;   :hints (("Goal" :in-theory (enable rdb))))


;; (defthm logcons-0
;;     (implies (bitp x)
;; 	     (equal (logcons x 0) x))
;;   :hints (("Goal" :in-theory (enable logcons))))

;; (defthm rdb-bitp
;;     (implies (bitp x)
;; 	     (equal (rdb (cons 1 0) x) x))
;;   :hints (("Goal" :in-theory (enable rdb))))

;; (defthm rdb-0
;;     (equal (rdb (cons 0 n) x) 0)
;;   :hints (("Goal" :in-theory (enable rdb bsp-size))))

;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;; Here begins a basic theory about lobops
;; ; Recursive definition of Logbit*.
;; (defthm logbit*
;;     (implies (and (integerp pos)
;; 		  (>= pos 0)
;; 		  (integerp i))
;; 	     (equal (logbit pos i)
;; 		    (if (equal pos 0)
;; 			(logcar i)
;; 			(logbit (1- pos) (logcdr i)))))
;;   :rule-classes :definition
;;   :hints (("Goal" :in-theory (e/d (logbit logbitp*) (logbitp)))))

;; (in-theory (disable logbit*))

;; (local
;; (defun logtail-induct (pos i)
;;   (if (zp pos)
;;       i
;;       (logtail-induct (1- pos) (logcdr i)))))


;; (defthm logcar-logtail
;;     (implies (and (integerp n) (<= 0 n)
;; 		  (integerp x))
;; 	     (equal (logcar (logtail n x))
;; 		    (logbit n x)))
;;   :hints (("Goal" :in-theory (e/d (logtail* logbit logbitp*)
;; 				  (logbitp))
;; 		  :induct (logtail-induct n x))))

;; (defthm logcdr-logtail
;;     (implies (and (integerp n) (<= 0 n)
;; 		  (integerp x))
;; 	     (equal (logcdr (logtail n x))
;; 		    (logtail (1+ n) x)))
;;   :hints (("Goal" :in-theory (enable logtail*)
;; 		    :induct (logtail-induct n x))))

;; ;; The following two lemmas are for expansion before BDD
;; (deflabel begin-bv-expand)
;; (defthm rdb-expand
;;    (implies (and (syntaxp (and (quoted-constant-p s) (quoted-constant-p n)))
;; 		 (integerp s) (< 0 s)
;; 		 (integerp n) (<= 0 n)
;; 		 (integerp x))
;; 	    (equal (rdb (cons s n) x)
;; 		   (logcons (logbit n x) (rdb (cons (1- s) (1+ n)) x))))
;;   :hints (("Goal" :in-theory (enable rdb bsp-position bsp-size loghead*
;; 				     logtail*))))


;; ;; logops supplement for logxxx operations. There are bunch of
;; ;; definition rules logior* and so on, but they are definition rules.
;; ;; We rewrite rules to forcibly open up the expressions before applying
;; ;; BDD techniques.  We redefine the same lemma as a rewrite rule.
;; (defthm open-logior-right-const
;;     (implies (and (bitp i1)
;; 		  (integerp i2)
;; 		  (integerp j))
;; 	     (equal (logior (logcons i1 i2) j)
;; 		    (logcons (b-ior i1 (logcar j)) (logior i2 (logcdr j)))))
;;   :hints (("Goal" :in-theory (enable logior*))))


;; (defthm open-logior-left-const
;;     (implies (and (bitp j1)
;; 		  (integerp j2)
;; 		  (integerp i))
;; 	     (equal (logior i (logcons j1 j2))
;; 		    (logcons (b-ior (logcar i) j1) (logior (logcdr i) j2))))
;;   :hints (("Goal" :in-theory (enable logior*))))

;; (defthm open-logior
;;     (implies (and (bitp i1)
;; 		  (bitp j1)
;; 		  (integerp i2)
;; 		  (integerp j2))
;; 	     (equal (logior (logcons i1 i2) (logcons j1 j2))
;; 		    (logcons (b-ior i1 j1) (logior i2 j2))))
;;   :hints (("Goal" :in-theory (enable logior*))))

;; (defthm open-logxor-right-const
;;     (implies (and (bitp i1)
;; 		  (integerp i2)
;; 		  (integerp j))
;; 	     (equal (logxor (logcons i1 i2) j)
;; 		    (logcons (b-xor i1 (logcar j)) (logxor i2 (logcdr j)))))
;;   :hints (("Goal" :in-theory (enable logxor*))))


;; (defthm open-logxor-left-const
;;     (implies (and (bitp j1)
;; 		  (integerp j2)
;; 		  (integerp i))
;; 	     (equal (logxor i (logcons j1 j2))
;; 		    (logcons (b-xor (logcar i) j1) (logxor (logcdr i) j2))))
;;   :hints (("Goal" :in-theory (enable logxor*))))

;; (defthm open-logxor
;;     (implies (and (bitp i1)
;; 		  (bitp j1)
;; 		  (integerp i2)
;; 		  (integerp j2))
;; 	     (equal (logxor (logcons i1 i2) (logcons j1 j2))
;; 		    (logcons (b-xor i1 j1) (logxor i2 j2))))
;;   :hints (("Goal" :in-theory (enable logxor*))))




;; (defthm open-logand-right-const
;;     (implies (and (bitp i1)
;; 		  (integerp i2)
;; 		  (integerp j))
;; 	     (equal (logand (logcons i1 i2) j)
;; 		    (logcons (b-and i1 (logcar j)) (logand i2 (logcdr j)))))
;;   :hints (("Goal" :in-theory (enable logand*))))


;; (defthm open-logand-left-const
;;     (implies (and (bitp j1)
;; 		  (integerp j2)
;; 		  (integerp i))
;; 	     (equal (logand i (logcons j1 j2))
;; 		    (logcons (b-and (logcar i) j1) (logand (logcdr i) j2))))
;;   :hints (("Goal" :in-theory (enable logand*))))

;; (defthm open-logand
;;     (implies (and (bitp i1)
;; 		  (bitp j1)
;; 		  (integerp i2)
;; 		  (integerp j2))
;; 	     (equal (logand (logcons i1 i2) (logcons j1 j2))
;; 		    (logcons (b-and i1 j1) (logand i2 j2))))
;;   :hints (("Goal" :in-theory (enable logand*))))

;; (defthm open-lognot
;;     (implies (and (bitp i1)
;; 		  (integerp i2))
;; 	     (equal (lognot (logcons i1 i2))
;; 		    (logcons (b-not i1) (lognot i2))))
;;   :hints (("Goal" :in-theory (enable lognot*))))

;; (defthm fold-logcdr-vector
;;     (implies (and (integerp x)
;; 		  (syntaxp (or (not (consp x))
;; 			       (not (equal (car x) 'logcons$inline)))))
;; 	     (equal (logcdr x) (logtail 1 x)))
;;   :hints (("goal" :in-theory (enable logtail*))))
;; (in-theory (disable fold-logcdr-vector))

;; (defthm fold-logcar-vector
;;     (implies (and (integerp x)
;; 		  (syntaxp (or (not (consp x))
;; 			       (not (equal (car x) 'logcons$inline)))))
;; 	     (equal (logcar x) (logbit 0 x)))
;;   :hints (("goal" :in-theory (e/d (logbit logbitp*)
;;                                   (logbitp)))))

;; (in-theory (disable fold-logcar-vector))
;; (deflabel end-bv-expand)

;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;; Bv-eqv rules
;; (defthm bv-eqv*
;;     (implies (and (integerp x)
;; 		  (integerp y)
;; 		  (integerp n)
;; 		  (>= n 0))
;; 	     (equal (bv-eqv n x y)
;; 		    (if (zp n)
;; 			1
;; 			(b-and (b-eqv (logcar x) (logcar y))
;; 			       (bv-eqv (1- n) (logcdr x) (logcdr y))))))
;;   :hints (("goal" :in-theory (enable bv-eqv loghead*)))
;;   :rule-classes :definition)

;; (in-theory (disable bv-eqv*))

;; ;; Following lemma is useful in converting a formula with 'bv-eqv' to one
;; ;; with 'equal'.
;; ;; This can cause BDD simplification to fail, especially if when the words
;; ;; need to be open up.
;; (defthm bv-eqv-iff-equal
;;   (implies (and (unsigned-byte-p n x) (unsigned-byte-p n y))
;; 	   (equal (b1p (bv-eqv n x y))
;; 		  (equal x y)))
;;   :hints (("Goal" :in-theory (enable bv-eqv b1p))))

;; (defthm bv-eqv-0
;;     (equal (bv-eqv 0 x y) 1)
;;   :Hints (("Goal" :in-theory (enable bv-eqv))))

;; (defthm bv-x-x
;;     (equal (bv-eqv n x x) 1)
;;   :hints (("goal" :in-theory (enable bv-eqv))))

;; (defthm bv-eqv-assoc
;;     (equal (bv-eqv n x y) (bv-eqv n y x))
;;   :hints (("Goal" :in-theory (enable bv-eqv))))

;; (defthm bv-eqv-bits
;;     (implies (and (bitp x) (bitp y) (integerp n) (> n 0))
;; 	     (equal (bv-eqv n x y) (b-eqv x y)))
;;   :hints (("Goal" :in-theory (enable bv-eqv* bitp bv-eqv-iff-equal))))

;; (defthm bv-eqv-expand
;;     (implies (and (integerp x) (integerp y)
;; 		  (integerp n) (> n 0)
;; 		  (syntaxp (quoted-constant-p n)))
;; 	     (equal (bv-eqv n x y)
;; 		    (b-and (b-eqv (logcar x) (logcar y))
;; 			   (bv-eqv (1- n) (logcdr x) (logcdr y)))))
;;   :hints (("Goal" :in-theory (enable bv-eqv*))))

;; ;; Following lemma is a schematic lemma which will be used in BDD proof.
;; ;; We noticed that several lemmas is a tautology under the property that
;; ;; (bv-eqv x y) and (bv-eqv x z) are not simultaneously asserted, if y and
;; ;; z are not equal. We instantiate the following lemma and add it to BDD
;; ;; proof as a hint.
;; (defthm bv-eqv-transitivity
;;     (implies (and (unsigned-byte-p n x)
;; 		  (unsigned-byte-p n y)
;; 		  (unsigned-byte-p n z)
;; 		  (b1p (b-and (bv-eqv n x z) (bv-eqv n y z))))
;; 	     (equal x y))
;;   :hints (("Goal" :in-theory (enable bv-eqv )))
;;   :rule-classes nil)

;; ;; Bv-expander is the theory to be enabled to expand bit vectors before
;; ;; applying bdd's.
;; (deftheory bv-expander
;;     '(rdb-expand
;;       open-lognot
;;       open-logand open-logand-right-const open-logand-left-const
;;       open-logior open-logior-right-const open-logior-left-const
;;       open-logxor open-logxor-right-const open-logxor-left-const
;;       fold-logcar-vector fold-logcdr-vector
;;       bv-eqv-bits
;;       bv-eqv-0
;;       bv-eqv-expand))

;; (in-theory (disable bv-expander))

;; (local (in-theory (enable b1p)))

;; ;; Bit-boolean-converter converting expressions of form (equal x 1) to
;; ;; expressions using bitp, lest BDD package assigns different boolean values
;; ;; to (b1p x) and (equal x 1).  It also converts (equal x 0) to (not (b1p x)).
;; (defthm equal-to-1-to-b1p
;;     (implies (bitp x)
;; 	     (equal (equal x 1)
;; 		    (b1p x)))
;;   :Hints (("Goal" :In-theory (enable bitp))))

;; (defthm equal-to-0-to-not-b1p
;;     (implies (bitp x)
;; 	     (equal (equal x 0)
;; 		    (not (b1p x))))
;;   :Hints (("Goal" :In-theory (enable bitp))))

;; (defthm equal-to-b1p-b-eqv
;;     (implies (and (bitp x) (bitp y))
;; 	     (equal (equal x y) (b1p (b-eqv x y))))
;;   :hints (("Goal" :in-theory (enable b-eqv b1p zbp bitp))))

;; (deftheory equal-b1p-converter
;;     '(equal-to-1-to-b1p equal-to-0-to-not-b1p))

;; (in-theory (disable equal-b1p-converter))
;; (in-theory (disable  equal-to-b1p-b-eqv))

;; ;; From here, we define bit-to-boolean converter, especially for BDD
;; ;; operation.
;; (deflabel begin-lift-b-ops)

;; (defthm zbp-b-and
;;     (equal (zbp (b-and x y))
;; 	   (or (zbp x) (zbp y)))
;;   :Hints (("Goal" :in-theory (enable b-and))))

;; (defthm zbp-b-ior
;;     (equal (zbp (b-ior x y))
;; 	   (and (zbp x) (zbp y)))
;;   :Hints (("Goal" :in-theory (enable b-ior))))

;; (defthm zbp-b-xor
;;     (equal (zbp (b-xor x y))
;; 	   (or (and (zbp x) (zbp y))
;; 	       (and (not (zbp x)) (not (zbp y)))))
;;   :Hints (("Goal" :in-theory (enable b-xor))))

;; (defthm zbp-b-not
;;     (equal (zbp (b-not x))
;; 	   (not (zbp x)))
;;   :Hints (("Goal" :in-theory (enable b-not))))

;; (defthm zbp-b-eqv
;;     (equal (zbp (b-eqv x y))
;; 	   (not (iff (zbp x) (zbp y))))
;;   :Hints (("Goal" :in-theory (enable b-eqv))))



;; (defthm b1p-b-and
;;     (equal (b1p (b-and x y))
;; 	   (and (b1p x) (b1p y)))
;;   :Hints (("Goal" :in-theory (enable b-and))))

;; (defthm b1p-b-ior
;;     (equal (b1p (b-ior x y))
;; 	   (or (b1p x) (b1p y)))
;;   :Hints (("Goal" :in-theory (enable b-ior))))

;; (defthm b1p-b-xor
;;     (equal (b1p (b-xor x y))
;; 	   (or (and (b1p x) (not (b1p y)))
;; 	       (and (not (b1p x)) (b1p y))))
;;   :Hints (("Goal" :in-theory (enable b-xor))))

;; (defthm b1p-b-not
;;     (equal (b1p (b-not x))
;; 	   (not (b1p x)))
;;   :Hints (("Goal" :in-theory (enable b-not))))

;; (defthm b1p-b-eqv
;;     (equal (b1p (b-eqv x y))
;; 	   (iff (b1p x) (b1p y)))
;;   :Hints (("Goal" :in-theory (enable b-eqv))))

;; (defthm b1p-nand (equal (b1p (b-nand x y)) (not (and (b1p x) (b1p y))))
;;   :hints (("Goal" :in-theory (enable b-nand))))

;; (defthm b1p-nor (equal (b1p (b-nor x y)) (not (or (b1p x) (b1p y))))
;;     :hints (("Goal" :in-theory (enable b-nor))))

;; (defthm b1p-andc1 (equal (b1p (b-andc1 x y)) (and (not (b1p x)) (b1p y)))
;;   :hints (("Goal" :in-theory (enable b-andc1))))

;; (defthm b1p-andc2 (equal (b1p (b-andc2 x y)) (and (b1p x) (not (b1p y))))
;;   :hints (("Goal" :in-theory (enable b-andc2))))

;; (defthm b1p-orc1 (equal (b1p (b-orc1 x y)) (or (not (b1p x)) (b1p y)))
;;   :hints (("Goal" :in-theory (enable b-orc1))))

;; (defthm b1p-orc2 (equal (b1p (b-orc2 x y)) (or (b1p x) (not (b1p y))))
;;   :hints (("Goal" :in-theory (enable b-orc2))))

;; (defthm zbp-to-b1p
;;     (equal (zbp x) (not (b1p x)))
;;   :hints (("Goal" :in-theory (enable b1p))))

;; (deflabel end-lift-b-ops)

;; (deftheory lift-b-ops
;;     (set-difference-theories (universal-theory 'end-lift-b-ops)
;; 			     (universal-theory 'begin-lift-b-ops)))

;; (in-theory (disable lift-b-ops))

;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ; New Simplifier
;; ; This simplifier simplifies bit terms into 1 and 0's using information
;; ; represented by b1p.
;; ; Origianl Simplify-Bit-Functions can simplify expressions with bit-functions
;; ; if its arguments are 0 or 1's.  For instance, it can reduce expressions
;; ; with a rule like:
;; ;  (EQUAL (B-AND 1 X) (BFIX X))
;; ; In the new simplifier reduces the expressions if hypothesis satisfies
;; ; certain conditions, like
;; ;	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; ;		  (equal (b-and x y) 0))
;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; (deflabel begin-b1p-bit-rewriter)

;; (defthm b1p-bit-forward
;;     (implies (and (b1p b) (force (bitp b))) (equal b 1))
;;   :hints (("goal" :in-theory (enable b1p bitp zbp)))
;;   :rule-classes :forward-chaining)

;; (defthm not-b1p-bit-forward
;;     (implies (and (not (b1p b)) (force (bitp b))) (equal b 0))
;;   :hints (("goal" :in-theory (enable b1p bitp zbp)))
;;   :rule-classes :forward-chaining)

;; (defthm simplify-bit-functions-2
;;     (and (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-and x y) 0))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-and x y) 0))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-and x y) y))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-and x y) x))

;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-ior x y) y))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-ior x y) x))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-ior x y) 1))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-ior x y) 1))

;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-xor x y) y))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-xor x y) x))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-xor x y) (b-not y)))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-xor x y) (b-not x)))

;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-eqv x y) (b-not y)))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-eqv x y) (b-not x)))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-eqv x y) y))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-eqv x y) x))

;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-nand x y) 1))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-nand x y) 1))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-nand x y) (b-not y)))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-nand x y) (b-not x)))

;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-nor x y) (b-not y)))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-nor x y) (b-not x)))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-nor x y) 0))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-nor x y) 0))

;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-andc1 x y) y))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-andc1 x y) 0))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-andc1 x y) 0))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-andc1 x y) (b-not x)))

;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-andc2 x y) 0))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-andc2 x y) x))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-andc2 x y) (b-not y)))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-andc2 x y) 0))

;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-orc1 x y) 1))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-orc1 x y) (b-not x)))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-orc1 x y) y))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-orc1 x y) 1))

;; 	 (implies (and (bitp x) (bitp y) (not (b1p x)))
;; 		  (equal (b-orc2 x y) (b-not y)))
;; 	 (implies (and (bitp x) (bitp y) (not (b1p y)))
;; 		  (equal (b-orc2 x y) 1))
;; 	 (implies (and (bitp x) (bitp y) (b1p x))
;; 		  (equal (b-orc2 x y) 1))
;; 	 (implies (and (bitp x) (bitp y) (b1p y))
;; 		  (equal (b-orc2 x y) x)))
;;   :hints (("Goal" :in-theory (enable b1p zbp b-and bitp))))

;; (deflabel end-b1p-bit-rewriter)

;; (deftheory b1p-bit-rewriter
;;     (set-difference-theories (universal-theory 'end-b1p-bit-rewriter)
;; 			     (universal-theory 'begin-b1p-bit-rewriter)))

;; (in-theory (disable b1p-bit-rewriter))
;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ; BDD helps
;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; (deftheory pre-bdd-disables
;;     '(bv-eqv-iff-equal simplify-bit-functions))

;; (deftheory bdd-disables
;;     '(bv-eqv-iff-equal simplify-bit-functions))

;; (theory-invariant (incompatible (:rewrite bv-eqv-iff-equal)
;; 				(:rewrite rdb-expand)))

;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ; range of unsigned-byte-p
;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ; theories about the range of unsigned-byte-p
;; (defthm plus-unsigned-byte-p-lt-2-*-expt-2-width
;;     (implies (and (unsigned-byte-p width val1)
;; 		  (unsigned-byte-p width val2))
;; 	     (< (+ val1 val2) (* 2 (expt 2 width))))
;;   :hints (("goal" :in-theory (enable unsigned-byte-p))))

;; (defun logbit-induction (pos val)
;;     (if (zp pos)
;; 	val
;; 	(logbit-induction (1- pos) (logcdr val))))

;; ; If a value are in the range  0 <= val < 2^width
;; ; then the width'th bit of val is not set.
;; (defthm logbit-0-if-val-lt-expt-2-width
;;     (implies (and (integerp width) (<= 0 width)
;; 		  (integerp val)
;; 		  (<= 0 val) (< val (expt 2 width)))
;; 	     (equal (logbit width val) 0))
;;   :hints (("goal" :in-theory (e/d (logbit* expt logcar logcdr)
;; 				  (exponents-add))
;; 		  :induct (logbit-induction width val)))
;;   :rule-classes nil)


;; (encapsulate nil
;; (local
;;  (defthm logbit-1-if-val-gt-expt-2-width-help1
;;      (IMPLIES (AND (INTEGERP WIDTH)
;; 		   (< 0 WIDTH)
;; 		   (INTEGERP VAL)
;; 		   (<= (* 2 (EXPT 2 (+ -1 WIDTH))) VAL)
;; 		   (< (/ VAL 2) (* 2 (EXPT 2 (+ -1 WIDTH)))))
;; 	      (> (* 2 (EXPT 2 (+ -1 WIDTH)))
;; 		 (FLOOR VAL 2)))
;;  :rule-classes nil))

;; (local
;;  (defthm logbit-1-if-val-gt-expt-2-width-help2
;;      (implies  (and (integerp val)
;; 		    (integerp width) (< 0 width)
;; 		    (< VAL (* 2 2 (EXPT 2 (+ -1 WIDTH)))))
;; 	       (< (/ VAL 2) (* 2 (EXPT 2 (+ -1 WIDTH)))))
;;    :hints (("goal" :in-theory (e/d (expt) (exponents-add))))
;;    :rule-classes nil))

;; (local
;; (defthm logbit-1-if-val-gt-expt-2-width-help
;;     (IMPLIES (AND (INTEGERP WIDTH)
;; 		  (INTEGERP VAL)
;; 		  (< 0 WIDTH)
;; 		  (<= (* 2 (EXPT 2 (+ -1 WIDTH))) (FLOOR VAL 2)))
;; 	     (<= (* 2 2 (EXPT 2 (+ -1 WIDTH))) VAL))
;;   :hints (("goal" :in-theory (e/d (exponents-add) (expt))
;; 		  :use ((:instance logbit-1-if-val-gt-expt-2-width-help1)
;; 			(:instance logbit-1-if-val-gt-expt-2-width-help2))))))


;; ; If a value are in the range  2^width <= val < 2^width * 2,
;; ; then the width'th bit of val is set.
;; (defthm logbit-1-if-val-gt-expt-2-width
;;     (implies (and (integerp width) (<= 0 width)
;; 		  (integerp val)
;; 		  (<= (expt 2 width) val)
;; 		  (< val (* 2 (expt 2 width))))
;; 	     (equal (logbit width val) 1))
;;   :hints (("goal" :in-theory (e/d (logbit* expt logcar logcdr)
;; 				  (exponents-add))
;; 		  :induct (logbit-induction width val)))
;;   :rule-classes nil)
;; )

;; ; Suppose val1 and val2 are unsigned-byte-p whose width is w.
;; ; If w'th bit of the sum (+ val1 val2) is not set,
;; ; (+ val1 val2) < 2^w.
;; (defthm plus-unsigned-byte-lt-expt-2-width-if-logbit
;;     (implies (and (unsigned-byte-p width val1)
;; 		  (unsigned-byte-p width val2)
;; 		  (not (b1p (logbit width (+ val1 val2)))))
;; 	     (< (+ val1 val2) (expt 2 width)))
;;   :hints (("goal" :in-theory (enable unsigned-byte-p)
;; 		  :use (:instance logbit-1-if-val-gt-expt-2-width
;; 				  (val (+ val1 val2))))))



;; ; Suppose val1 and val2 are unsigned-byte-p whose width is w.
;; ; If w'th bit of the sum (+ val1 val2) is set, then
;; ;   2^w < (+ val1 val2).
;; (defthm plus-unsigned-byte-gt-expt-2-width-if-logbit
;;     (implies (and (unsigned-byte-p width val1)
;; 		  (unsigned-byte-p width val2)
;; 		  (b1p (logbit width (+ val1 val2))))
;; 	     (<= (expt 2 width) (+ val1 val2)))
;;   :hints (("goal" :in-theory (enable unsigned-byte-p)
;; 		  :use (:instance logbit-0-if-val-lt-expt-2-width
;; 				  (val (+ val1 val2))))))

;; ; Suppose val1 and val2 are unsigned-byte-p whose width is w.
;; ; If the sum of val1 and val2 does not carry out to w'th bit,
;; ;  (loghead w (+ val1 val2)) = (+ val1 val2)
;; (defthm loghead-unsigned-byte-+-if-not-carry
;;     (implies (and (integerp width)
;; 		  (<= 0 width)
;; 		  (unsigned-byte-p width val1)
;; 		  (unsigned-byte-p width val2)
;; 		  (not (b1p (logbit width (+ val1 val2)))))
;; 	     (equal (loghead width (+ val1 val2)) (+ val1 val2)))
;;   :hints (("goal" :in-theory (e/d (loghead)
;;                                   (bfix))
;; 		  :do-not-induct t)))

;; (encapsulate nil
;; (local
;; (defthm j*k-ge-2*k-if-j-gt-1
;;     (implies (and (integerp j)
;; 		  (< 1 j)
;; 		  (integerp k)
;; 		  (< 0 k))
;; 	     (<= (* 2 k) (* j k)))
;;   :hints (("Goal" :in-theory (enable <-*-right-cancel)))
;;   :rule-classes :linear))

;; ; A trivia theorem.
;; ; If y < x < 2*y, then (x mod y) = x - y
;; (defthm mod-x-y-=-minux-x-y
;;  (implies (and (integerp x) (integerp y) (< 0 y)
;; 	       (<= y x) (< x (* 2 y)))
;; 	  (equal (mod x y) (- x y)))
;;  :Hints (("goal" :in-theory (disable (:generalize floor-bounds)))
;; 	 ("subgoal 1" :cases ((<= j 1)))))
;; )

;; (in-theory (disable mod-x-y-=-minux-x-y))

;; ; Suppose val1 and val2 are unsigned-byte-p whose width is w.
;; ; If the sum of val1 and val2 does not carry out to w'th bit,
;; ;  (loghead w (+ val1 val2)) = (+ val1 val2)
;; (defthm loghead-unsigned-byte-+-if-carry
;;     (implies (and (integerp width)
;; 		  (<= 0 width)
;; 		  (unsigned-byte-p width val1)
;; 		  (unsigned-byte-p width val2)
;; 		  (b1p (logbit width (+ val1 val2))))
;; 	     (equal (loghead width (+ val1 val2))
;; 		    (- (+ val1 val2) (expt 2 width))))
;;   :hints (("goal" :in-theory (enable loghead mod-x-y-=-minux-x-y)
;; 		  :do-not-induct t)))