		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec-part-select

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

Definitions and Theorems

Function: s4vec-part-select

(defun s4vec-part-select (lsb width in)
  (declare (xargs :guard (and (s4vec-p lsb)
                              (s4vec-p width)
                              (s4vec-p in))))
  (let ((__function__ 's4vec-part-select))
    (declare (ignorable __function__))
    (b* (((unless (and (s4vec-2vec-p lsb)
                       (s4vec-2vec-p width)))
          (s4vec-x))
         (widthint (s4vec->upper width))
         ((when (sparseint-< widthint 0))
          (s4vec-x))
         (lsbint (s4vec->upper lsb))
         ((unless (sparseint-< lsbint 0))
          (s4vec-zero-ext width (s4vec-rsh lsb in))))
      (s4vec-zero-ext
           width
           (s4vec-concat (s2vec (sparseint-unary-minus lsbint))
                         (s4vec-x)
                         in)))))

Theorem: s4vec-p-of-s4vec-part-select

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

Theorem: s4vec-part-select-correct

(defthm s4vec-part-select-correct
  (b* ((?res (s4vec-part-select lsb width in)))
    (equal (s4vec->4vec res)
           (4vec-part-select (s4vec->4vec lsb)
                             (s4vec->4vec width)
                             (s4vec->4vec in)))))

Theorem: s4vec-part-select-of-s4vec-fix-lsb

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

Theorem: s4vec-part-select-s4vec-equiv-congruence-on-lsb

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

Theorem: s4vec-part-select-of-s4vec-fix-width

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

Theorem: s4vec-part-select-s4vec-equiv-congruence-on-width

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

Theorem: s4vec-part-select-of-s4vec-fix-in

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

Theorem: s4vec-part-select-s4vec-equiv-congruence-on-in

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