• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
      • Bitops
        • Bitops/merge
        • Bitops-compatibility
        • Bitops-books
        • Logbitp-reasoning
        • Bitops/signed-byte-p
          • Basic-signed-byte-p-of-binary-minus
          • Basic-unsigned-byte-p-of-*
          • Basic-signed-byte-p-of-*
          • Basic-signed-byte-p-of-unary-minus
          • Basic-signed-byte-p-of-mixed-*
          • Basic-unsigned-byte-p-of-+-with-cin
          • Lousy-signed-byte-p-of-*
          • Lousy-signed-byte-p-of-mixed-*
          • Basic-signed-byte-p-of-+-with-cin
          • Basic-signed-byte-p-of-unary-minus-2
          • Lousy-unsigned-byte-p-of-*-mixed
          • Lousy-unsigned-byte-p-of-*
          • Basic-signed-byte-p-of-+
          • Basic-signed-byte-p-of-truncate-split
          • Basic-unsigned-byte-p-of-+
          • Basic-signed-byte-p-of-floor-split
          • Basic-signed-byte-p-of-truncate
          • Basic-signed-byte-p-of-floor
          • Unsigned-byte-p-of-minus-when-signed-byte-p
          • Signed-byte-p-of-decrement-when-natural-signed-byte-p
          • Unsigned-byte-p-of-abs-when-signed-byte-p
          • Signed-byte-p-when-unsigned-byte-p-smaller
          • Signed-byte-p-when-signed-byte-p-smaller
          • Signed-byte-p-of-loghead
          • Basic-unsigned-byte-p-of-truncate
          • Basic-unsigned-byte-p-of-rem
          • Basic-unsigned-byte-p-of-mod
          • Basic-unsigned-byte-p-of-floor
          • Basic-signed-byte-p-of-rem
          • Basic-signed-byte-p-of-mod
          • Basic-signed-byte-p-of-lognot
          • Basic-signed-byte-p-of-1+lognot
        • Fast-part-select
        • Bitops/integer-length
        • Bitops/extra-defs
        • Install-bit
        • Trailing-0-count
        • Bitops/defaults
        • Logbitp-mismatch
        • Trailing-1-count
        • Bitops/rotate
        • Bitops/equal-by-logbitp
        • Bitops/ash-bounds
        • Bitops/fast-logrev
        • Limited-shifts
        • Bitops/part-select
        • Bitops/parity
        • Bitops/saturate
        • Bitops/part-install
        • Bitops/logbitp-bounds
        • Bitops/ihsext-basics
        • Bitops/fast-rotate
        • Bitops/fast-logext
        • Bitops/ihs-extensions
      • Bv
      • Ihs
      • Rtl
    • Algebra
  • Testing-utilities

• Bitops/signed-byte-p

Basic-unsigned-byte-p-of-+-with-cin

Adding N-bit unsigneds with a carry bit creates an N+1 bit unsigned.

ACL2's fancy unification stuff means this works fine in the common case that you're dealing with quoted constants for N and N+1. See also basic-unsigned-byte-p-of-+.

Definitions and Theorems

Theorem: basic-unsigned-byte-p-of-+-with-cin

(defthm basic-unsigned-byte-p-of-+-with-cin
  (implies (and (bitp cin)
                (unsigned-byte-p n a)
                (unsigned-byte-p n b))
           (unsigned-byte-p (+ 1 n) (+ cin a b)))
  :rule-classes
  ((:rewrite)
   (:rewrite :corollary (implies (and (bitp cin)
                                      (unsigned-byte-p n a)
                                      (unsigned-byte-p n b))
                                 (unsigned-byte-p (+ 1 n)
                                                  (+ a b cin))))))