		Search-engine friendly clone of the ACL2 documentation.

4vec-operations

4vec-part-select

Part select operation: select width bits of in starting at lsb.

Signature
(4vec-part-select lsb width in) → res
Arguments: lsb — Guard (4vec-p lsb).; width — Guard (4vec-p width).; in — Guard (4vec-p in).
Returns: res — Type (4vec-p res).

Definitions and Theorems

Function: 4vec-part-select

(defun 4vec-part-select (lsb width in)
  (declare (xargs :guard (and (4vec-p lsb)
                              (4vec-p width)
                              (4vec-p in))))
  (let ((__function__ '4vec-part-select))
    (declare (ignorable __function__))
    (if (and (2vec-p lsb)
             (2vec-p width)
             (<= 0 (2vec->val width)))
        (b* ((lsbval (2vec->val lsb))
             ((when (<= 0 lsbval))
              (4vec-zero-ext width (4vec-rsh lsb in))))
          (4vec-zero-ext width
                         (4vec-concat (2vec (- lsbval))
                                      (4vec-x)
                                      in)))
      (4vec-x))))

Theorem: 4vec-p-of-4vec-part-select

(defthm 4vec-p-of-4vec-part-select
  (b* ((res (4vec-part-select lsb width in)))
    (4vec-p res))
  :rule-classes :rewrite)

Theorem: 4vec-part-select-of-2vecx-fix-lsb

(defthm 4vec-part-select-of-2vecx-fix-lsb
  (equal (4vec-part-select (2vecx-fix lsb)
                           width in)
         (4vec-part-select lsb width in)))

Theorem: 4vec-part-select-2vecx-equiv-congruence-on-lsb

(defthm 4vec-part-select-2vecx-equiv-congruence-on-lsb
  (implies (2vecx-equiv lsb lsb-equiv)
           (equal (4vec-part-select lsb width in)
                  (4vec-part-select lsb-equiv width in)))
  :rule-classes :congruence)

Theorem: 4vec-part-select-of-2vecx-fix-width

(defthm 4vec-part-select-of-2vecx-fix-width
  (equal (4vec-part-select lsb (2vecx-fix width)
                           in)
         (4vec-part-select lsb width in)))

Theorem: 4vec-part-select-2vecx-equiv-congruence-on-width

(defthm 4vec-part-select-2vecx-equiv-congruence-on-width
  (implies (2vecx-equiv width width-equiv)
           (equal (4vec-part-select lsb width in)
                  (4vec-part-select lsb width-equiv in)))
  :rule-classes :congruence)

Theorem: 4vec-part-select-of-4vec-fix-in

(defthm 4vec-part-select-of-4vec-fix-in
  (equal (4vec-part-select lsb width (4vec-fix in))
         (4vec-part-select lsb width in)))

Theorem: 4vec-part-select-4vec-equiv-congruence-on-in

(defthm 4vec-part-select-4vec-equiv-congruence-on-in
  (implies (4vec-equiv in in-equiv)
           (equal (4vec-part-select lsb width in)
                  (4vec-part-select lsb width in-equiv)))
  :rule-classes :congruence)