		Search-engine friendly clone of the ACL2 documentation.

Limited-shifts

Limshift-logext-of-logapp

Computes (loghead full-width (logapp concat-width x y)).

Signature
(limshift-logext-of-logapp full-width concat-width x y) → shifted
Arguments: full-width — Guard (posp full-width).; concat-width — Guard (natp concat-width).; x — Guard (integerp x).; y — Guard (integerp y).
Returns: shifted — Type (integerp shifted).

Definitions and Theorems

Function: limshift-logext-of-logapp

(defun limshift-logext-of-logapp (full-width concat-width x y)
 (declare (xargs :guard (and (posp full-width)
                             (natp concat-width)
                             (integerp x)
                             (integerp y))))
 (let ((__function__ 'limshift-logext-of-logapp))
   (declare (ignorable __function__))
   (b*
     ((concat-width (lnfix concat-width))
      (full-width (lposfix full-width))
      (x (lifix x))
      (y (lifix y))
      (concat-width-limited (logcollapse (integer-length full-width)
                                         concat-width)))
     (logext full-width
             (logapp concat-width-limited x y)))))

Theorem: integerp-of-limshift-logext-of-logapp

(defthm integerp-of-limshift-logext-of-logapp
 (b* ((shifted
           (limshift-logext-of-logapp full-width concat-width x y)))
   (integerp shifted))
 :rule-classes :type-prescription)

Theorem: limshift-logext-of-logapp-correct

(defthm limshift-logext-of-logapp-correct
  (equal (limshift-logext-of-logapp full-width concat-width x y)
         (logext full-width (logapp concat-width x y))))