		Search-engine friendly clone of the ACL2 documentation.

S4vecs

S4vec-part-install

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

Definitions and Theorems

Function: s4vec-part-install

(defun s4vec-part-install (lsb width in val)
 (declare (xargs :guard (and (s4vec-p lsb)
                             (s4vec-p width)
                             (s4vec-p in)
                             (s4vec-p val))))
 (let ((__function__ 's4vec-part-install))
   (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-concat
            lsb in
            (s4vec-concat
                 width val
                 (s4vec-rsh (s2vec (sparseint-plus lsbint widthint))
                            in))))
      (neg-lsb (sparseint-unary-minus lsbint))
      ((unless (sparseint-< neg-lsb widthint))
       (s4vec-fix in))
      (width+lsb (sparseint-plus lsbint widthint)))
     (s4vec-concat (s2vec width+lsb)
                   (s4vec-rsh (s2vec neg-lsb) val)
                   (s4vec-rsh (s2vec width+lsb) in)))))

Theorem: s4vec-p-of-s4vec-part-install

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

Theorem: s4vec-part-install-correct

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem: s4vec-part-install-of-s4vec-fix-val

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

Theorem: s4vec-part-install-s4vec-equiv-congruence-on-val

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