Returns the width of a range
Function:
(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:
(defthm posp-of-vl-selwidth (b* ((w (vl-selwidth a b))) (posp w)) :rule-classes :type-prescription)
Theorem:
(defthm vl-selwidth-of-nfix-a (equal (vl-selwidth (nfix a) b) (vl-selwidth a b)))
Theorem:
(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:
(defthm vl-selwidth-of-nfix-b (equal (vl-selwidth a (nfix b)) (vl-selwidth a b)))
Theorem:
(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)