		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Carry-out-bit

Signature
(carry-out-bit xbit ybit sumbit) → cout
Arguments: xbit — Guard (bitp xbit).; ybit — Guard (bitp ybit).; sumbit — Guard (bitp sumbit).
Returns: cout — Type (bitp cout).

Definitions and Theorems

Function: carry-out-bit

(defun carry-out-bit (xbit ybit sumbit)
  (declare (xargs :guard (and (bitp xbit)
                              (bitp ybit)
                              (bitp sumbit))))
  (let ((__function__ 'carry-out-bit))
    (declare (ignorable __function__))
    (b-ior (b-and xbit ybit)
           (b-and (b-ior xbit ybit)
                  (b-not sumbit)))))

Theorem: bitp-of-carry-out-bit

(defthm bitp-of-carry-out-bit
  (b* ((cout (carry-out-bit xbit ybit sumbit)))
    (bitp cout))
  :rule-classes :type-prescription)

Theorem: carry-out-bit-correct

(defthm carry-out-bit-correct
 (implies (and (posp width)
               (bitp cin)
               (integerp x1)
               (integerp y1)
               (integerp x2)
               (integerp y2)
               (equal xbit (logbit (1- width) x1))
               (equal ybit (logbit (1- width) y1))
               (equal sumbit
                      (logbit (1- width) (+ cin x1 y1))))
          (equal (logapp width (+ cin x1 y1)
                         (+ x2 y2 (carry-out-bit xbit ybit sumbit)))
                 (+ cin (logapp width x1 x2)
                    (logapp width y1 y2)))))

Theorem: carry-out-bit-correct-logtail

(defthm carry-out-bit-correct-logtail
  (implies
       (and (posp width)
            (bitp cin)
            (integerp x)
            (integerp y))
       (equal (logtail width (+ x y cin))
              (+ (logtail width x)
                 (logtail width y)
                 (carry-out-bit (logbit (1- width) x)
                                (logbit (1- width) y)
                                (logbit (1- width) (+ cin x y))))))
  :rule-classes nil)

Theorem: carry-out-bit-of-bfix-xbit

(defthm carry-out-bit-of-bfix-xbit
  (equal (carry-out-bit (bfix xbit) ybit sumbit)
         (carry-out-bit xbit ybit sumbit)))

Theorem: carry-out-bit-bit-equiv-congruence-on-xbit

(defthm carry-out-bit-bit-equiv-congruence-on-xbit
  (implies (bit-equiv xbit xbit-equiv)
           (equal (carry-out-bit xbit ybit sumbit)
                  (carry-out-bit xbit-equiv ybit sumbit)))
  :rule-classes :congruence)

Theorem: carry-out-bit-of-bfix-ybit

(defthm carry-out-bit-of-bfix-ybit
  (equal (carry-out-bit xbit (bfix ybit) sumbit)
         (carry-out-bit xbit ybit sumbit)))

Theorem: carry-out-bit-bit-equiv-congruence-on-ybit

(defthm carry-out-bit-bit-equiv-congruence-on-ybit
  (implies (bit-equiv ybit ybit-equiv)
           (equal (carry-out-bit xbit ybit sumbit)
                  (carry-out-bit xbit ybit-equiv sumbit)))
  :rule-classes :congruence)

Theorem: carry-out-bit-of-bfix-sumbit

(defthm carry-out-bit-of-bfix-sumbit
  (equal (carry-out-bit xbit ybit (bfix sumbit))
         (carry-out-bit xbit ybit sumbit)))

Theorem: carry-out-bit-bit-equiv-congruence-on-sumbit

(defthm carry-out-bit-bit-equiv-congruence-on-sumbit
  (implies (bit-equiv sumbit sumbit-equiv)
           (equal (carry-out-bit xbit ybit sumbit)
                  (carry-out-bit xbit ybit sumbit-equiv)))
  :rule-classes :congruence)