		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-plus

Signature
(sparseint$-plus x y) → sum
Arguments: x — Guard (sparseint$-p x).; y — Guard (sparseint$-p y).
Returns: sum — Type (sparseint$-p sum).

Definitions and Theorems

Function: sparseint$-plus$inline

(defun sparseint$-plus$inline (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$-plus))
    (declare (ignorable __function__))
    (b* (((mv sum ?height)
          (sparseint$-plus-offset x (sparseint$-height x)
                                  0 y (sparseint$-height y)
                                  0)))
      sum)))

Theorem: sparseint$-p-of-sparseint$-plus

(defthm sparseint$-p-of-sparseint$-plus
  (b* ((sum (sparseint$-plus$inline x y)))
    (sparseint$-p sum))
  :rule-classes :rewrite)

Theorem: sparseint$-height-correctp-of-sparseint$-plus

(defthm sparseint$-height-correctp-of-sparseint$-plus
  (b* ((?sum (sparseint$-plus$inline x y)))
    (implies (and (sparseint$-height-correctp x)
                  (sparseint$-height-correctp y))
             (sparseint$-height-correctp sum))))

Theorem: sparseint$-val-of-sparseint$-plus

(defthm sparseint$-val-of-sparseint$-plus
  (b* ((?sum (sparseint$-plus$inline x y)))
    (equal (sparseint$-val sum)
           (+ (sparseint$-val x)
              (sparseint$-val y)))))

Theorem: sparseint$-plus$inline-of-sparseint$-fix-x

(defthm sparseint$-plus$inline-of-sparseint$-fix-x
  (equal (sparseint$-plus$inline (sparseint$-fix x)
                                 y)
         (sparseint$-plus$inline x y)))

Theorem: sparseint$-plus$inline-sparseint$-equiv-congruence-on-x

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

Theorem: sparseint$-plus$inline-of-sparseint$-fix-y

(defthm sparseint$-plus$inline-of-sparseint$-fix-y
  (equal (sparseint$-plus$inline x (sparseint$-fix y))
         (sparseint$-plus$inline x y)))

Theorem: sparseint$-plus$inline-sparseint$-equiv-congruence-on-y

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