		Search-engine friendly clone of the ACL2 documentation.

Range-tools

Vl-selwidth

Returns the width of a range [a:b], i.e., |a-b|+1.

Signature
(vl-selwidth a b) → w
Arguments: a — Guard (natp a).; b — Guard (natp b).
Returns: w — Type (posp w).

Definitions and Theorems

Function: vl-selwidth

(defun vl-selwidth (a b)
       (declare (xargs :guard (and (natp a) (natp b))))
       (let ((__function__ 'vl-selwidth))
            (declare (ignorable __function__))
            (+ 1 (abs (- (nfix a) (nfix b))))))

Theorem: posp-of-vl-selwidth

(defthm posp-of-vl-selwidth
        (b* ((w (vl-selwidth a b))) (posp w))
        :rule-classes :type-prescription)

Theorem: vl-selwidth-of-nfix-a

(defthm vl-selwidth-of-nfix-a
        (equal (vl-selwidth (nfix a) b)
               (vl-selwidth a b)))

Theorem: vl-selwidth-nat-equiv-congruence-on-a

(defthm vl-selwidth-nat-equiv-congruence-on-a
        (implies (acl2::nat-equiv a a-equiv)
                 (equal (vl-selwidth a b)
                        (vl-selwidth a-equiv b)))
        :rule-classes :congruence)

Theorem: vl-selwidth-of-nfix-b

(defthm vl-selwidth-of-nfix-b
        (equal (vl-selwidth a (nfix b))
               (vl-selwidth a b)))

Theorem: vl-selwidth-nat-equiv-congruence-on-b

(defthm vl-selwidth-nat-equiv-congruence-on-b
        (implies (acl2::nat-equiv b b-equiv)
                 (equal (vl-selwidth a b)
                        (vl-selwidth a b-equiv)))
        :rule-classes :congruence)