		Search-engine friendly clone of the ACL2 documentation.

Vex2-byte1

!vex2-byte1->r

Update the |ACL2|::|R| field of a vex2-byte1 bit structure.

Signature
(!vex2-byte1->r r x) → new-x
Arguments: r — Guard (bitp r).; x — Guard (vex2-byte1-p x).
Returns: new-x — Type (vex2-byte1-p new-x).

Definitions and Theorems

Function: !vex2-byte1->r$inline

(defun !vex2-byte1->r$inline (r x)
 (declare (xargs :guard (and (bitp r) (vex2-byte1-p x))))
 (mbe :logic
      (b* ((r (mbe :logic (bfix r) :exec r))
           (x (vex2-byte1-fix x)))
        (part-install r x :width 1 :low 7))
      :exec (the (unsigned-byte 8)
                 (logior (the (unsigned-byte 8)
                              (logand (the (unsigned-byte 8) x)
                                      (the (signed-byte 9) -129)))
                         (the (unsigned-byte 8)
                              (ash (the (unsigned-byte 1) r) 7))))))

Theorem: vex2-byte1-p-of-!vex2-byte1->r

(defthm vex2-byte1-p-of-!vex2-byte1->r
  (b* ((new-x (!vex2-byte1->r$inline r x)))
    (vex2-byte1-p new-x))
  :rule-classes :rewrite)

Theorem: !vex2-byte1->r$inline-of-bfix-r

(defthm !vex2-byte1->r$inline-of-bfix-r
  (equal (!vex2-byte1->r$inline (bfix r) x)
         (!vex2-byte1->r$inline r x)))

Theorem: !vex2-byte1->r$inline-bit-equiv-congruence-on-r

(defthm !vex2-byte1->r$inline-bit-equiv-congruence-on-r
  (implies (bit-equiv r r-equiv)
           (equal (!vex2-byte1->r$inline r x)
                  (!vex2-byte1->r$inline r-equiv x)))
  :rule-classes :congruence)

Theorem: !vex2-byte1->r$inline-of-vex2-byte1-fix-x

(defthm !vex2-byte1->r$inline-of-vex2-byte1-fix-x
  (equal (!vex2-byte1->r$inline r (vex2-byte1-fix x))
         (!vex2-byte1->r$inline r x)))

Theorem: !vex2-byte1->r$inline-vex2-byte1-equiv-congruence-on-x

(defthm !vex2-byte1->r$inline-vex2-byte1-equiv-congruence-on-x
  (implies (vex2-byte1-equiv x x-equiv)
           (equal (!vex2-byte1->r$inline r x)
                  (!vex2-byte1->r$inline r x-equiv)))
  :rule-classes :congruence)

Theorem: !vex2-byte1->r-is-vex2-byte1

(defthm !vex2-byte1->r-is-vex2-byte1
  (equal (!vex2-byte1->r r x)
         (change-vex2-byte1 x :r r)))

Theorem: vex2-byte1->r-of-!vex2-byte1->r

(defthm vex2-byte1->r-of-!vex2-byte1->r
  (b* ((?new-x (!vex2-byte1->r$inline r x)))
    (equal (vex2-byte1->r new-x) (bfix r))))

Theorem: !vex2-byte1->r-equiv-under-mask

(defthm !vex2-byte1->r-equiv-under-mask
  (b* ((?new-x (!vex2-byte1->r$inline r x)))
    (vex2-byte1-equiv-under-mask new-x x 127)))