		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-equal-width

Signature
(sparseint$-equal-width width x y-offset y) → equal
Arguments: width — Guard (posp width).; x — Guard (sparseint$-p x).; y-offset — Guard (natp y-offset).; y — Guard (sparseint$-p y).
Returns: equal — Type (booleanp equal).

Definitions and Theorems

Function: sparseint$-equal-width

(defun sparseint$-equal-width (width x y-offset y)
 (declare (xargs :guard (and (posp width)
                             (sparseint$-p x)
                             (natp y-offset)
                             (sparseint$-p y))))
 (let ((__function__ 'sparseint$-equal-width))
  (declare (ignorable __function__))
  (b* ((width (lposfix width))
       (y-offset (lnfix y-offset)))
   (sparseint$-case
    x
    :leaf
    (sparseint$-case
        y
        :leaf (equal (bignum-logext width x.val)
                     (bignum-logext width (logtail y-offset y.val)))
        :concat (sparseint$-equal-int-width
                     width
                     y-offset y (bignum-logext width x.val)))
    :concat
    (sparseint$-case
         y :leaf
         (sparseint$-equal-int-width
              width 0 x
              (bignum-logext width (logtail y-offset y.val)))
         :concat
         (b* (((when (<= width x.width))
               (sparseint$-equal-width width x.lsbs y-offset y))
              ((when (<= y.width y-offset))
               (sparseint$-equal-width width x (- y-offset y.width)
                                       y.msbs))
              (y-width1 (- y.width y-offset))
              ((when (<= width y-width1))
               (sparseint$-equal-width width x y-offset y.lsbs)))
           (and (sparseint$-equal-width x.width x.lsbs y-offset y)
                (sparseint$-equal-width (- width x.width)
                                        x.msbs (+ x.width y-offset)
                                        y))))))))

Theorem: booleanp-of-sparseint$-equal-width

(defthm booleanp-of-sparseint$-equal-width
  (b* ((equal (sparseint$-equal-width width x y-offset y)))
    (booleanp equal))
  :rule-classes :type-prescription)

Theorem: sparseint$-equal-width-correct

(defthm sparseint$-equal-width-correct
  (b* ((common-lisp::?equal
            (sparseint$-equal-width width x y-offset y)))
    (equal equal
           (equal (logext width (sparseint$-val x))
                  (logext width
                          (logtail y-offset (sparseint$-val y)))))))

Theorem: sparseint$-equal-width-of-pos-fix-width

(defthm sparseint$-equal-width-of-pos-fix-width
  (equal (sparseint$-equal-width (pos-fix width)
                                 x y-offset y)
         (sparseint$-equal-width width x y-offset y)))

Theorem: sparseint$-equal-width-pos-equiv-congruence-on-width

(defthm sparseint$-equal-width-pos-equiv-congruence-on-width
 (implies (pos-equiv width width-equiv)
          (equal (sparseint$-equal-width width x y-offset y)
                 (sparseint$-equal-width width-equiv x y-offset y)))
 :rule-classes :congruence)

Theorem: sparseint$-equal-width-of-sparseint$-fix-x

(defthm sparseint$-equal-width-of-sparseint$-fix-x
  (equal (sparseint$-equal-width width (sparseint$-fix x)
                                 y-offset y)
         (sparseint$-equal-width width x y-offset y)))

Theorem: sparseint$-equal-width-sparseint$-equiv-congruence-on-x

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

Theorem: sparseint$-equal-width-of-nfix-y-offset

(defthm sparseint$-equal-width-of-nfix-y-offset
  (equal (sparseint$-equal-width width x (nfix y-offset)
                                 y)
         (sparseint$-equal-width width x y-offset y)))

Theorem: sparseint$-equal-width-nat-equiv-congruence-on-y-offset

(defthm sparseint$-equal-width-nat-equiv-congruence-on-y-offset
 (implies (nat-equiv y-offset y-offset-equiv)
          (equal (sparseint$-equal-width width x y-offset y)
                 (sparseint$-equal-width width x y-offset-equiv y)))
 :rule-classes :congruence)

Theorem: sparseint$-equal-width-of-sparseint$-fix-y

(defthm sparseint$-equal-width-of-sparseint$-fix-y
 (equal (sparseint$-equal-width width x y-offset (sparseint$-fix y))
        (sparseint$-equal-width width x y-offset y)))

Theorem: sparseint$-equal-width-sparseint$-equiv-congruence-on-y

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