• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
        • Sparseint-impl
          • Sparseint$-binary-bitop-width
          • Sparseint$-plus-width
          • Sparseint$-binary-bitop-offset
          • Sparseint$-binary-bitop-int-width
          • Sparseint$-plus-int-width
          • Sum-with-cin
          • Sparseint$-plus-offset
          • Sparseint$-binary-bitop-int
          • Sparseint$-finalize-concat
          • Sparseint$-plus-int
          • Sparseint$-binary-bittest-width
          • Sparseint$-binary-bittest-int-width
          • Sparseint$-trailing-0-count-width
          • Sparseint$-height
          • Int-to-sparseint$-rec
          • Carry-out
          • Sparseint$-compare-width
          • Sparseint$-binary-bittest-offset
          • Sparseint$-equal-width
          • Sparseint$-binary-bittest-int
          • Sparseint$-compare-int-width
          • Sparseint$-bitcount-width
          • Sparseint$-unary-bittest-width
          • Sparseint$-rightshift-rec
          • Sparseint$-equal-int-width
          • Sparseint$-trailing-0-count-rec
          • Sparseint$-unary-bitop
          • Sparseint$-concatenate
          • Sparseint$-length-width-rec
          • Sparseint$-sign-ext
          • Sparseint$-binary-bitop
          • Binary-bitop
          • Sparseint$-compare-offset
          • Sparseint$-unary-bittest-offset
          • Sparseint$-equal-offset
          • Sparseint$-truncate
          • Sparseint$-mergeable-leaves-p
          • Carry-out-bit
          • Sparseint$-truncate-height
          • Sparseint$-compare-int
          • Sparseint$-binary-bittest
          • Sparseint$-equal-int
          • Sparseint$-rightshift
          • Sparseint$-leaves-mergeable-p
          • Sparseint$-plus
          • Unary-bitop
          • Sparseint$-bitcount-rec
          • Within-1
          • Sparseint$
          • Binary-bitop-cofactor2
          • Binary-bitop-cofactor1
          • Sparseint$-compare
          • Sparseint$-unary-bittest
          • Sparseint$-height-correct-exec
          • Sparseint$-equal
          • Sparseint$-bitnot
          • Sparseint$-unary-minus
          • Sparseint$-bit
          • Int-to-sparseint$
          • Binary-bittest
          • Sparseint$-length-rec
          • Sparseint$-val
          • Binary-bitop-swap
          • Compare
          • Sparseint$-real-height
          • Sparseint$-height-correctp
          • Sparseint$-length
        • Sparseint-p
        • Sparseint-binary-bittest
        • Sparseint-concatenate
        • Sparseint-binary-bitop
        • Sparseint-bitite
        • Sparseint-fix
        • Sparseint$-binary-minus
        • Sparseint-trailing-1-count-from
        • Sparseint-trailing-0-count-from
        • Sparseint-equal
        • Sparseint-test-bitorc2
        • Sparseint-test-bitorc1
        • Sparseint-test-bitnand
        • Sparseint-test-bitandc2
        • Sparseint-test-bitandc1
        • Sparseint-test-bitand
        • Sparseint-rightshift
        • Sparseint-bitcount-from
        • Sparseint-test-bitxor
        • Sparseint-test-bitor
        • Sparseint-test-bitnor
        • Sparseint-test-biteqv
        • Sparseint-compare
        • Sparseint-binary-minus
        • Sparseint-sign-ext
        • Sparseint-plus
        • Sparseint-bitandc2
        • Sparseint-bitandc1
        • Sparseint-bitand
        • Sparseint$-leaf-bitlimit
        • Sparseint-bitxor
        • Sparseint-bitorc2
        • Sparseint-bitorc1
        • Sparseint-bitor
        • Sparseint-bitnor
        • Sparseint-bitnand
        • Sparseint-biteqv
        • Sparseint-ash
        • Sparseint-<
        • Sparseint-bit
        • Sparseint-trailing-1-count
        • Sparseint-trailing-0-count
        • Sparseint-unary-minus
        • Sparseint-length
        • Sparseint-bitnot
        • Sparseint-bitcount
        • Int-to-sparseint
        • Sparseint-val
      • Bitops
      • Bv
      • Ihs
      • Rtl
    • Algebra
  • Testing-utilities

• Sparseint-impl

Sum-with-cin

Signature

(sum-with-cin cin x y) → sum

Arguments

cin — Guard (bitp cin).

x — Guard (integerp x).

y — Guard (integerp y).

Returns

sum — Type (integerp sum).

Definitions and Theorems

Function: sum-with-cin

(defun sum-with-cin (cin x y)
  (declare (xargs :guard (and (bitp cin)
                              (integerp x)
                              (integerp y))))
  (let ((__function__ 'sum-with-cin))
    (declare (ignorable __function__))
    (+ (lbfix cin) (lifix x) (lifix y))))

Theorem: integerp-of-sum-with-cin

(defthm integerp-of-sum-with-cin
  (b* ((sum (sum-with-cin cin x y)))
    (integerp sum))
  :rule-classes :type-prescription)

Theorem: logext-of-sum-with-cin-simplify-arg1

(defthm logext-of-sum-with-cin-simplify-arg1
  (implies (and (equal xx (logext width x))
                (bind-free (case-match xx
                             (('logext w xxx)
                              (if (equal w width)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (logext width xxx)
                       (logext width xx)))
           (equal (logext width (sum-with-cin cin x y))
                  (logext width (sum-with-cin cin xxx y)))))

Theorem: logext-of-sum-with-cin-simplify-arg2

(defthm logext-of-sum-with-cin-simplify-arg2
  (implies (and (equal xx (logext width x))
                (bind-free (case-match xx
                             (('logext w xxx)
                              (if (equal w width)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (logext width xxx)
                       (logext width xx)))
           (equal (logext width (sum-with-cin cin y x))
                  (logext width (sum-with-cin cin y xxx)))))

Theorem: loghead-of-sum-with-cin-simplify-arg1

(defthm loghead-of-sum-with-cin-simplify-arg1
  (implies (and (equal xx (loghead width x))
                (bind-free (case-match xx
                             (('acl2::loghead$inline w xxx)
                              (if (equal w width)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (loghead width xxx)
                       (loghead width xx)))
           (equal (loghead width (sum-with-cin cin x y))
                  (loghead width (sum-with-cin cin xxx y)))))

Theorem: loghead-of-sum-with-cin-simplify-arg2

(defthm loghead-of-sum-with-cin-simplify-arg2
  (implies (and (equal xx (loghead width x))
                (bind-free (case-match xx
                             (('acl2::loghead$inline w xxx)
                              (if (equal w width)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (loghead width xxx)
                       (loghead width xx)))
           (equal (loghead width (sum-with-cin cin y x))
                  (loghead width (sum-with-cin cin y xxx)))))

Theorem: logapp-of-sum-with-cin-simplify-arg1

(defthm logapp-of-sum-with-cin-simplify-arg1
  (implies (and (equal xx (loghead width x))
                (bind-free (case-match xx
                             (('acl2::loghead$inline w xxx)
                              (if (equal w width)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (loghead width xxx)
                       (loghead width xx)))
           (equal (logapp width (sum-with-cin cin x y) z)
                  (logapp width (sum-with-cin cin xxx y)
                          z))))

Theorem: logapp-of-sum-with-cin-simplify-arg2

(defthm logapp-of-sum-with-cin-simplify-arg2
  (implies (and (equal xx (loghead width x))
                (bind-free (case-match xx
                             (('acl2::loghead$inline w xxx)
                              (if (equal w width)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (loghead width xxx)
                       (loghead width xx)))
           (equal (logapp width (sum-with-cin cin y x) z)
                  (logapp width (sum-with-cin cin y xxx)
                          z))))

Theorem: logbitp-of-sum-with-cin-simplify-arg1

(defthm logbitp-of-sum-with-cin-simplify-arg1
  (implies (and (equal ww (+ 1 (nfix width)))
                (equal xx (loghead ww x))
                (bind-free (case-match xx
                             (('acl2::loghead$inline w xxx)
                              (if (equal w ww)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (loghead ww xxx)
                       (loghead ww xx)))
           (equal (logbitp width (sum-with-cin cin x y))
                  (logbitp width (sum-with-cin cin xxx y)))))

Theorem: logbitp-of-sum-with-cin-simplify-arg2

(defthm logbitp-of-sum-with-cin-simplify-arg2
  (implies (and (equal ww (+ 1 (nfix width)))
                (equal xx (loghead ww x))
                (bind-free (case-match xx
                             (('acl2::loghead$inline w xxx)
                              (if (equal w ww)
                                  (if (equal xxx x)
                                      nil
                                    (cons (cons 'xxx xxx) 'nil))
                                (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil))))
                             (& (and (not (equal xx x))
                                     (cons (cons 'xxx xx) 'nil)))))
                (equal (loghead ww xxx)
                       (loghead ww xx)))
           (equal (logbitp width (sum-with-cin cin y x))
                  (logbitp width (sum-with-cin cin y xxx)))))

Theorem: sum-with-cin-of-bfix-cin

(defthm sum-with-cin-of-bfix-cin
  (equal (sum-with-cin (bfix cin) x y)
         (sum-with-cin cin x y)))

Theorem: sum-with-cin-bit-equiv-congruence-on-cin

(defthm sum-with-cin-bit-equiv-congruence-on-cin
  (implies (bit-equiv cin cin-equiv)
           (equal (sum-with-cin cin x y)
                  (sum-with-cin cin-equiv x y)))
  :rule-classes :congruence)

Theorem: sum-with-cin-of-ifix-x

(defthm sum-with-cin-of-ifix-x
  (equal (sum-with-cin cin (ifix x) y)
         (sum-with-cin cin x y)))

Theorem: sum-with-cin-int-equiv-congruence-on-x

(defthm sum-with-cin-int-equiv-congruence-on-x
  (implies (int-equiv x x-equiv)
           (equal (sum-with-cin cin x y)
                  (sum-with-cin cin x-equiv y)))
  :rule-classes :congruence)

Theorem: sum-with-cin-of-ifix-y

(defthm sum-with-cin-of-ifix-y
  (equal (sum-with-cin cin x (ifix y))
         (sum-with-cin cin x y)))

Theorem: sum-with-cin-int-equiv-congruence-on-y

(defthm sum-with-cin-int-equiv-congruence-on-y
  (implies (int-equiv y y-equiv)
           (equal (sum-with-cin cin x y)
                  (sum-with-cin cin x y-equiv)))
  :rule-classes :congruence)