• 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-signed-byte-p-of-binary-minus

Subtracting N-bit signeds creates an N+1 bit signed.

ACL2's fancy unification stuff means this works fine in the common case that you're dealing with quoted constants.

You might ask, why have this rule when we have rules like basic-signed-byte-p-of-+? After all, (- a b) is just the same as (+ a (unary-- b)). The answer is: the rule about (signed-byte-p (unary-- x)), basic-signed-byte-p-of-unary-minus, isn't very nice because of , and doesn't give us doesn't really give us an indirect way to get here.

See also basic-signed-byte-p-of-unary-minus and basic-signed-byte-p-of-unary-minus-2.

Definitions and Theorems

Theorem: basic-signed-byte-p-of-binary-minus

(defthm basic-signed-byte-p-of-binary-minus
  (implies (and (signed-byte-p n a)
                (signed-byte-p n b))
           (signed-byte-p (+ 1 n) (- a b))))