		Search-engine friendly clone of the ACL2 documentation.

Svex-select

Svex-select-to-lhs

Signature
(svex-select-to-lhs x) → lhs
Arguments: x — Guard (svex-select-p x).
Returns: lhs — Type (lhs-p lhs).

Definitions and Theorems

Function: svex-select-to-lhs

(defun svex-select-to-lhs (x)
 (declare (xargs :guard (svex-select-p x)))
 (declare (xargs :guard (svex-select-staticp x)))
 (let ((__function__ 'svex-select-to-lhs))
  (declare (ignorable __function__))
  (svex-select-case
   x :var
   (if (eql x.width 0)
       nil
     (list (make-lhrange :atom (make-lhatom-var :name x.name :rsh 0)
                         :w x.width)))
   :part
   (b* ((inner-lhs (svex-select-to-lhs x.subexp))
        (rsh (2vec->val (svex-quote->val x.lsb))))
     (lhs-rsh rsh
              (lhs-concat (+ rsh x.width)
                          inner-lhs nil))))))

Theorem: lhs-p-of-svex-select-to-lhs

(defthm lhs-p-of-svex-select-to-lhs
  (b* ((lhs (svex-select-to-lhs x)))
    (lhs-p lhs))
  :rule-classes :rewrite)

Theorem: lhs-vars-of-svex-select-to-lhs

(defthm lhs-vars-of-svex-select-to-lhs
  (b* ((?lhs (svex-select-to-lhs x)))
    (implies (not (equal v (svex-select-inner-var x)))
             (not (member v (lhs-vars lhs))))))

Theorem: svex-select-to-lhs-of-svex-select-fix-x

(defthm svex-select-to-lhs-of-svex-select-fix-x
  (equal (svex-select-to-lhs (svex-select-fix x))
         (svex-select-to-lhs x)))

Theorem: svex-select-to-lhs-svex-select-equiv-congruence-on-x

(defthm svex-select-to-lhs-svex-select-equiv-congruence-on-x
  (implies (svex-select-equiv x x-equiv)
           (equal (svex-select-to-lhs x)
                  (svex-select-to-lhs x-equiv)))
  :rule-classes :congruence)