		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-equal-offset

Signature
(sparseint$-equal-offset x y-offset y) → equal
Arguments: 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-offset

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

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

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

Theorem: sparseint$-equal-offset-correct

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

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

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

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

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

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

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

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

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

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

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

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

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