		Search-engine friendly clone of the ACL2 documentation.

Sparseint

Sparseint-sign-ext

Sign-extend the given sparseint at the given (positive) position

Signature
(sparseint-sign-ext n x) → ext
Arguments: n — Guard (posp n).; x — Guard (sparseint-p x).
Returns: ext — Type (sparseint-p ext).

Definitions and Theorems

Function: sparseint-sign-ext

(defun sparseint-sign-ext (n x)
  (declare (xargs :guard (and (posp n) (sparseint-p x))))
  (let ((__function__ 'sparseint-sign-ext))
    (declare (ignorable __function__))
    (b* ((x (sparseint-fix x))
         ((mv ans ?height)
          (sparseint$-sign-ext n x (sparseint$-height x))))
      ans)))

Theorem: sparseint-p-of-sparseint-sign-ext

(defthm sparseint-p-of-sparseint-sign-ext
  (b* ((ext (sparseint-sign-ext n x)))
    (sparseint-p ext))
  :rule-classes :rewrite)

Theorem: sparseint-sign-ext-correct

(defthm sparseint-sign-ext-correct
  (b* nil
    (equal (sparseint-val (sparseint-sign-ext n x))
           (logext n (sparseint-val x)))))

Theorem: sparseint-sign-ext-of-pos-fix-n

(defthm sparseint-sign-ext-of-pos-fix-n
  (equal (sparseint-sign-ext (pos-fix n) x)
         (sparseint-sign-ext n x)))

Theorem: sparseint-sign-ext-pos-equiv-congruence-on-n

(defthm sparseint-sign-ext-pos-equiv-congruence-on-n
  (implies (pos-equiv n n-equiv)
           (equal (sparseint-sign-ext n x)
                  (sparseint-sign-ext n-equiv x)))
  :rule-classes :congruence)

Theorem: sparseint-sign-ext-of-sparseint-fix-x

(defthm sparseint-sign-ext-of-sparseint-fix-x
  (equal (sparseint-sign-ext n (sparseint-fix x))
         (sparseint-sign-ext n x)))

Theorem: sparseint-sign-ext-sparseint-equiv-congruence-on-x

(defthm sparseint-sign-ext-sparseint-equiv-congruence-on-x
  (implies (sparseint-equiv x x-equiv)
           (equal (sparseint-sign-ext n x)
                  (sparseint-sign-ext n x-equiv)))
  :rule-classes :congruence)