(vl-echarlist-unsigned-value-aux x radix n) → *
Function:
(defun vl-echarlist-unsigned-value-aux (x radix n) (declare (xargs :guard (and (vl-echarlist-p x) (natp radix) (equal n (len x))))) (declare (xargs :guard (and (<= 2 radix) (<= radix 36)))) (let ((__function__ 'vl-echarlist-unsigned-value-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) 0) (car-digit (vl-echar-digit-value (car x) radix)) ((unless car-digit) nil) (cdr-value (vl-echarlist-unsigned-value-aux (cdr x) radix (1- n))) ((unless cdr-value) nil)) (+ (* (expt (lnfix radix) (1- n)) car-digit) cdr-value))))
Theorem:
(defthm vl-echarlist-unsigned-value-aux-of-vl-echarlist-fix-x (equal (vl-echarlist-unsigned-value-aux (vl-echarlist-fix x) radix n) (vl-echarlist-unsigned-value-aux x radix n)))
Theorem:
(defthm vl-echarlist-unsigned-value-aux-vl-echarlist-equiv-congruence-on-x (implies (vl-echarlist-equiv x x-equiv) (equal (vl-echarlist-unsigned-value-aux x radix n) (vl-echarlist-unsigned-value-aux x-equiv radix n))) :rule-classes :congruence)
Theorem:
(defthm vl-echarlist-unsigned-value-aux-of-nfix-radix (equal (vl-echarlist-unsigned-value-aux x (nfix radix) n) (vl-echarlist-unsigned-value-aux x radix n)))
Theorem:
(defthm vl-echarlist-unsigned-value-aux-nat-equiv-congruence-on-radix (implies (acl2::nat-equiv radix radix-equiv) (equal (vl-echarlist-unsigned-value-aux x radix n) (vl-echarlist-unsigned-value-aux x radix-equiv n))) :rule-classes :congruence)