		Search-engine friendly clone of the ACL2 documentation.

Svstmt-compile.lisp

4vec-replace-range

Signature
(4vec-replace-range x &key lsb width val) → new-x
Arguments: x — the non-replaced part.
Guard (4vec-p x).; lsb — Guard (natp lsb).; width — Guard (natp width).; val — Guard (4vec-p val).
Returns: new-x — Type (4vec-p new-x).

Definitions and Theorems

Function: 4vec-replace-range-fn

(defun 4vec-replace-range-fn (x lsb width val)
  (declare (xargs :guard (and (4vec-p x)
                              (natp lsb)
                              (natp width)
                              (4vec-p val))))
  (let ((__function__ '4vec-replace-range))
    (declare (ignorable __function__))
    (b* ((high-part (4vec-rsh (2vec (+ (lnfix width) (lnfix lsb)))
                              x))
         (new+high (4vec-concat (2vec (lnfix width))
                                val high-part)))
      (4vec-concat (2vec (lnfix lsb))
                   x new+high))))

Theorem: 4vec-p-of-4vec-replace-range

(defthm 4vec-p-of-4vec-replace-range
  (b* ((new-x (4vec-replace-range-fn x lsb width val)))
    (4vec-p new-x))
  :rule-classes :rewrite)

Theorem: 4vec-replace-range-fn-of-4vec-fix-x

(defthm 4vec-replace-range-fn-of-4vec-fix-x
  (equal (4vec-replace-range-fn (4vec-fix x)
                                lsb width val)
         (4vec-replace-range-fn x lsb width val)))

Theorem: 4vec-replace-range-fn-4vec-equiv-congruence-on-x

(defthm 4vec-replace-range-fn-4vec-equiv-congruence-on-x
  (implies (4vec-equiv x x-equiv)
           (equal (4vec-replace-range-fn x lsb width val)
                  (4vec-replace-range-fn x-equiv lsb width val)))
  :rule-classes :congruence)

Theorem: 4vec-replace-range-fn-of-nfix-lsb

(defthm 4vec-replace-range-fn-of-nfix-lsb
  (equal (4vec-replace-range-fn x (nfix lsb)
                                width val)
         (4vec-replace-range-fn x lsb width val)))

Theorem: 4vec-replace-range-fn-nat-equiv-congruence-on-lsb

(defthm 4vec-replace-range-fn-nat-equiv-congruence-on-lsb
  (implies (nat-equiv lsb lsb-equiv)
           (equal (4vec-replace-range-fn x lsb width val)
                  (4vec-replace-range-fn x lsb-equiv width val)))
  :rule-classes :congruence)

Theorem: 4vec-replace-range-fn-of-nfix-width

(defthm 4vec-replace-range-fn-of-nfix-width
  (equal (4vec-replace-range-fn x lsb (nfix width)
                                val)
         (4vec-replace-range-fn x lsb width val)))

Theorem: 4vec-replace-range-fn-nat-equiv-congruence-on-width

(defthm 4vec-replace-range-fn-nat-equiv-congruence-on-width
  (implies (nat-equiv width width-equiv)
           (equal (4vec-replace-range-fn x lsb width val)
                  (4vec-replace-range-fn x lsb width-equiv val)))
  :rule-classes :congruence)

Theorem: 4vec-replace-range-fn-of-4vec-fix-val

(defthm 4vec-replace-range-fn-of-4vec-fix-val
  (equal (4vec-replace-range-fn x lsb width (4vec-fix val))
         (4vec-replace-range-fn x lsb width val)))

Theorem: 4vec-replace-range-fn-4vec-equiv-congruence-on-val

(defthm 4vec-replace-range-fn-4vec-equiv-congruence-on-val
  (implies (4vec-equiv val val-equiv)
           (equal (4vec-replace-range-fn x lsb width val)
                  (4vec-replace-range-fn x lsb width val-equiv)))
  :rule-classes :congruence)