		Search-engine friendly clone of the ACL2 documentation.

Sparseint-impl

Sparseint$-binary-bittest-offset

Signature
(sparseint$-binary-bittest-offset op x y-offset y) → test
Arguments: op — Guard (integerp op).; x — Guard (sparseint$-p x).; y-offset — Guard (natp y-offset).; y — Guard (sparseint$-p y).
Returns: test — Type (booleanp test).

Definitions and Theorems

Function: sparseint$-binary-bittest-offset

(defun sparseint$-binary-bittest-offset (op x y-offset y)
 (declare (type (unsigned-byte 4) op))
 (declare (xargs :guard (and (integerp op)
                             (sparseint$-p x)
                             (natp y-offset)
                             (sparseint$-p y))))
 (let ((__function__ 'sparseint$-binary-bittest-offset))
  (declare (ignorable __function__))
  (b* ((y-offset (lnfix y-offset)))
   (sparseint$-case
    x
    :leaf
    (sparseint$-case
       y
       :leaf (binary-bittest op x.val (logtail y-offset y.val))
       :concat (sparseint$-binary-bittest-int (binary-bitop-swap op)
                                              y-offset y x.val))
    :concat
    (sparseint$-case
     y :leaf
     (sparseint$-binary-bittest-int op 0 x (logtail y-offset y.val))
     :concat
     (b*
      (((when (<= y.width y-offset))
        (sparseint$-binary-bittest-offset op x (- y-offset y.width)
                                          y.msbs)))
      (or (sparseint$-binary-bittest-width
               op x.width x.lsbs y-offset y)
          (sparseint$-binary-bittest-offset
               op x.msbs (+ x.width y-offset)
               y))))))))

Theorem: booleanp-of-sparseint$-binary-bittest-offset

(defthm booleanp-of-sparseint$-binary-bittest-offset
  (b* ((test (sparseint$-binary-bittest-offset op x y-offset y)))
    (booleanp test))
  :rule-classes :type-prescription)

Theorem: sparseint$-val-of-sparseint$-binary-bittest-offset

(defthm sparseint$-val-of-sparseint$-binary-bittest-offset
  (b* ((?test (sparseint$-binary-bittest-offset op x y-offset y)))
    (equal test
           (binary-bittest op (sparseint$-val x)
                           (logtail y-offset (sparseint$-val y))))))

Theorem: sparseint$-binary-bittest-offset-of-ifix-op

(defthm sparseint$-binary-bittest-offset-of-ifix-op
  (equal (sparseint$-binary-bittest-offset (ifix op)
                                           x y-offset y)
         (sparseint$-binary-bittest-offset op x y-offset y)))

Theorem: sparseint$-binary-bittest-offset-int-equiv-congruence-on-op

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

Theorem: sparseint$-binary-bittest-offset-of-sparseint$-fix-x

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

Theorem: sparseint$-binary-bittest-offset-sparseint$-equiv-congruence-on-x

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

Theorem: sparseint$-binary-bittest-offset-of-nfix-y-offset

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

Theorem: sparseint$-binary-bittest-offset-nat-equiv-congruence-on-y-offset

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

Theorem: sparseint$-binary-bittest-offset-of-sparseint$-fix-y

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

Theorem: sparseint$-binary-bittest-offset-sparseint$-equiv-congruence-on-y

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