		Search-engine friendly clone of the ACL2 documentation.

Svex-select

Svex-select-count

Measure for recurring over svex-select structures.

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

Definitions and Theorems

Function: svex-select-count

(defun svex-select-count (x)
 (declare (xargs :guard (svex-select-p x)))
 (let ((__function__ 'svex-select-count))
   (declare (ignorable __function__))
   (case (svex-select-kind x)
     (:var 1)
     (:part (+ 4
               (svex-select-count (svex-select-part->subexp x)))))))

Theorem: natp-of-svex-select-count

(defthm natp-of-svex-select-count
  (b* ((count (svex-select-count x)))
    (natp count))
  :rule-classes :type-prescription)

Theorem: svex-select-count-of-svex-select-fix-x

(defthm svex-select-count-of-svex-select-fix-x
  (equal (svex-select-count (svex-select-fix x))
         (svex-select-count x)))

Theorem: svex-select-count-svex-select-equiv-congruence-on-x

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

Theorem: svex-select-count-of-svex-select-part

(defthm svex-select-count-of-svex-select-part
  (implies
       t
       (< (+ (svex-select-count subexp))
          (svex-select-count (svex-select-part lsb width subexp))))
  :rule-classes :linear)

Theorem: svex-select-count-of-svex-select-part->subexp

(defthm svex-select-count-of-svex-select-part->subexp
  (implies (equal (svex-select-kind x) :part)
           (< (svex-select-count (svex-select-part->subexp x))
              (svex-select-count x)))
  :rule-classes :linear)