		Search-engine friendly clone of the ACL2 documentation.

Limited-shifts

Limshift-loghead-of-logsquash

Computes (loghead full-width (logsquash squash-width x)).

Signature
(limshift-loghead-of-logsquash full-width squash-width x) → shifted
Arguments: full-width — Guard (natp full-width).; squash-width — Guard (natp squash-width).; x — Guard (integerp x).
Returns: shifted — Type (integerp shifted).

Definitions and Theorems

Function: limshift-loghead-of-logsquash

(defun limshift-loghead-of-logsquash (full-width squash-width x)
 (declare (xargs :guard (and (natp full-width)
                             (natp squash-width)
                             (integerp x))))
 (let ((__function__ 'limshift-loghead-of-logsquash))
   (declare (ignorable __function__))
   (b*
     ((squash-width (lnfix squash-width))
      (full-width (lnfix full-width))
      (x (lifix x))
      (squash-width-limited (logcollapse (integer-length full-width)
                                         squash-width)))
     (loghead full-width
              (logsquash squash-width-limited x)))))

Theorem: integerp-of-limshift-loghead-of-logsquash

(defthm integerp-of-limshift-loghead-of-logsquash
  (b*
   ((shifted
         (limshift-loghead-of-logsquash full-width squash-width x)))
   (integerp shifted))
  :rule-classes :type-prescription)

Theorem: limshift-loghead-of-logsquash-correct

(defthm limshift-loghead-of-logsquash-correct
  (equal (limshift-loghead-of-logsquash full-width squash-width x)
         (loghead full-width (logsquash squash-width x))))