(vlsv-aggregate-aliases name width lsb) → aliases
Function:
(defun vlsv-aggregate-aliases (name width lsb) (declare (xargs :guard (and (sv::name-p name) (posp width) (maybe-natp lsb)))) (let ((__function__ 'vlsv-aggregate-aliases)) (declare (ignorable __function__)) (append-without-guard (vlsv-aggregate-subalias name width) (and lsb (vlsv-aggregate-superalias name width lsb)))))
Theorem:
(defthm lhspairs-p-of-vlsv-aggregate-aliases (b* ((aliases (vlsv-aggregate-aliases name width lsb))) (sv::lhspairs-p aliases)) :rule-classes :rewrite)
Theorem:
(defthm vlsv-aggregate-aliases-vars (b* ((?aliases (vlsv-aggregate-aliases name width lsb))) (sv::svarlist-addr-p (sv::lhspairs-vars aliases))))
Theorem:
(defthm vlsv-aggregate-aliases-of-name-fix-name (equal (vlsv-aggregate-aliases (sv::name-fix name) width lsb) (vlsv-aggregate-aliases name width lsb)))
Theorem:
(defthm vlsv-aggregate-aliases-name-equiv-congruence-on-name (implies (sv::name-equiv name name-equiv) (equal (vlsv-aggregate-aliases name width lsb) (vlsv-aggregate-aliases name-equiv width lsb))) :rule-classes :congruence)
Theorem:
(defthm vlsv-aggregate-aliases-of-pos-fix-width (equal (vlsv-aggregate-aliases name (pos-fix width) lsb) (vlsv-aggregate-aliases name width lsb)))
Theorem:
(defthm vlsv-aggregate-aliases-pos-equiv-congruence-on-width (implies (acl2::pos-equiv width width-equiv) (equal (vlsv-aggregate-aliases name width lsb) (vlsv-aggregate-aliases name width-equiv lsb))) :rule-classes :congruence)
Theorem:
(defthm vlsv-aggregate-aliases-of-maybe-natp-fix-lsb (equal (vlsv-aggregate-aliases name width (maybe-natp-fix lsb)) (vlsv-aggregate-aliases name width lsb)))
Theorem:
(defthm vlsv-aggregate-aliases-maybe-nat-equiv-congruence-on-lsb (implies (acl2::maybe-nat-equiv lsb lsb-equiv) (equal (vlsv-aggregate-aliases name width lsb) (vlsv-aggregate-aliases name width lsb-equiv))) :rule-classes :congruence)