		Search-engine friendly clone of the ACL2 documentation.

Limited-shifts

Limshift-loghead-of-logapp

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

Signature
(limshift-loghead-of-logapp full-width concat-width x y) → shifted
Arguments: full-width — Guard (natp 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-loghead-of-logapp

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

Theorem: integerp-of-limshift-loghead-of-logapp

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

Theorem: limshift-loghead-of-logapp-correct

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