Encoding Redundant Representations
Function:
(defun gamma (i a b c) (if (zp i) (bitn c 0) (logior (bitn a (+ -1 (* 2 i))) (bitn b (+ -1 (* 2 i))))))
Function:
(defun delta (i a b c d) (if (zp i) (bitn d 0) (logand (logior (logand (bitn a (+ -2 (* 2 i))) (bitn b (+ -2 (* 2 i)))) (logior (logand (bitn a (+ -2 (* 2 i))) (gamma (1- i) a b c)) (logand (bitn b (+ -2 (* 2 i))) (gamma (1- i) a b c)))) (lognot (logxor (bitn a (1- (* 2 i))) (bitn b (1- (* 2 i))))))))
Function:
(defun psi (i a b c d) (if (not (natp i)) 0 (+ (bits a (1+ (* 2 i)) (* 2 i)) (bits b (1+ (* 2 i)) (* 2 i)) (gamma i a b c) (delta i a b c d) (* -4 (+ (gamma (1+ i) a b c) (delta (1+ i) a b c d))))))
Theorem:
(defthm psi-m-1 (implies (and (natp m) (>= m 1) (bvecp a (- (* 2 m) 2)) (bvecp b (- (* 2 m) 2)) (bvecp c 1) (bvecp d 1)) (and (equal (gamma m a b c) 0) (equal (delta m a b c d) 0) (>= (psi (1- m) a b c d) 0))) :rule-classes nil)
Function:
(defun sum-psi (m a b c d) (if (zp m) 0 (+ (* (expt 2 (* 2 (1- m))) (psi (1- m) a b c d)) (sum-psi (1- m) a b c d))))
Theorem:
(defthm sum-psi-lemma (implies (and (natp m) (<= 1 m) (bvecp a (- (* 2 m) 2)) (bvecp b (- (* 2 m) 2)) (bvecp c 1) (bvecp d 1)) (equal (+ a b c d) (sum-psi m a b c d))) :rule-classes nil)
Theorem:
(defthm psi-bnd (and (integerp (psi i a b c d)) (<= (psi i a b c d) 2) (>= (psi i a b c d) -2)))
Function:
(defun pp4-psi (i x a b c d n) (if (zerop i) (cat 1 1 (bitn (lognot (neg (psi i a b c d))) 0) 1 (bmux4 (psi i a b c d) x n) n) (cat 1 1 (bitn (lognot (neg (psi i a b c d))) 0) 1 (bmux4 (psi i a b c d) x n) n 0 1 (neg (psi (1- i) a b c d)) 1 0 (* 2 (1- i)))))
Function:
(defun sum-pp4-psi (x a b c d m n) (if (zp m) 0 (+ (pp4-psi (1- m) x a b c d n) (sum-pp4-psi x a b c d (1- m) n))))
Theorem:
(defthm redundant-booth (implies (and (natp m) (<= 1 m) (not (zp n)) (bvecp x (1- n)) (bvecp a (- (* 2 m) 2)) (bvecp b (- (* 2 m) 2)) (bvecp c 1) (bvecp d 1) (= y (+ a b c d))) (= (+ (expt 2 n) (sum-pp4-psi x a b c d m n)) (+ (expt 2 (+ n (* 2 m))) (* x y)))) :rule-classes nil)