• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
    • 100-theorems
    • Arithmetic
    • Bit-vectors
      • Sparseint
        • Sparseint-impl
        • 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

Sparseint$-binary-minus

Subtract one sparseint from another.

Signature

(sparseint$-binary-minus x y) → minus

Arguments

x — Guard (sparseint$-p x).

y — Guard (sparseint$-p y).

Returns

minus — Type (sparseint$-p minus).

Definitions and Theorems

Function: sparseint$-binary-minus

(defun sparseint$-binary-minus (x y)
  (declare (xargs :guard (and (sparseint$-p x)
                              (sparseint$-p y))))
  (declare (xargs :guard (and (sparseint$-height-correctp x)
                              (sparseint$-height-correctp y))))
  (let ((__function__ 'sparseint$-binary-minus))
    (declare (ignorable __function__))
    (b* ((x.height (sparseint$-height x))
         (y.height (sparseint$-height y))
         (y.neg (sparseint$-bitnot y))
         ((mv minus ?height)
          (sparseint$-plus-offset x x.height 0 y.neg y.height 1)))
      minus)))

Theorem: sparseint$-p-of-sparseint$-binary-minus

(defthm sparseint$-p-of-sparseint$-binary-minus
  (b* ((minus (sparseint$-binary-minus x y)))
    (sparseint$-p minus))
  :rule-classes :rewrite)

Theorem: sparseint$-height-correctp-of-sparseint$-binary-minus

(defthm sparseint$-height-correctp-of-sparseint$-binary-minus
  (b* ((?minus (sparseint$-binary-minus x y)))
    (implies (and (sparseint$-height-correctp x)
                  (sparseint$-height-correctp y))
             (sparseint$-height-correctp minus))))

Theorem: sparseint$-val-of-sparseint$-binary-minus

(defthm sparseint$-val-of-sparseint$-binary-minus
  (b* ((?minus (sparseint$-binary-minus x y)))
    (equal (sparseint$-val minus)
           (- (sparseint$-val x)
              (sparseint$-val y)))))

Theorem: sparseint$-binary-minus-of-sparseint$-fix-x

(defthm sparseint$-binary-minus-of-sparseint$-fix-x
  (equal (sparseint$-binary-minus (sparseint$-fix x)
                                  y)
         (sparseint$-binary-minus x y)))

Theorem: sparseint$-binary-minus-sparseint$-equiv-congruence-on-x

(defthm sparseint$-binary-minus-sparseint$-equiv-congruence-on-x
  (implies (sparseint$-equiv x x-equiv)
           (equal (sparseint$-binary-minus x y)
                  (sparseint$-binary-minus x-equiv y)))
  :rule-classes :congruence)

Theorem: sparseint$-binary-minus-of-sparseint$-fix-y

(defthm sparseint$-binary-minus-of-sparseint$-fix-y
  (equal (sparseint$-binary-minus x (sparseint$-fix y))
         (sparseint$-binary-minus x y)))

Theorem: sparseint$-binary-minus-sparseint$-equiv-congruence-on-y

(defthm sparseint$-binary-minus-sparseint$-equiv-congruence-on-y
  (implies (sparseint$-equiv y y-equiv)
           (equal (sparseint$-binary-minus x y)
                  (sparseint$-binary-minus x y-equiv)))
  :rule-classes :congruence)