(vlsv-aggregate-superalias name width lsb) → alias
Function:
(defun vlsv-aggregate-superalias (name width lsb) (declare (xargs :guard (and (sv::name-p name) (posp width) (natp lsb)))) (let ((__function__ 'vlsv-aggregate-superalias)) (declare (ignorable __function__)) (b* ((var (sv::make-simple-svar name)) (lhs (sv::make-simple-lhs :width width :var var)) (outervar (sv::make-simple-svar :self)) (outerlhs (sv::make-simple-lhs :width width :var outervar :rsh lsb))) (list (cons lhs outerlhs)))))
Theorem:
(defthm lhspairs-p-of-vlsv-aggregate-superalias (b* ((alias (vlsv-aggregate-superalias name width lsb))) (sv::lhspairs-p alias)) :rule-classes :rewrite)
Theorem:
(defthm vlsv-aggregate-superalias-vars (b* ((?alias (vlsv-aggregate-superalias name width lsb))) (sv::svarlist-addr-p (sv::lhspairs-vars alias))))
Theorem:
(defthm vlsv-aggregate-superalias-of-name-fix-name (equal (vlsv-aggregate-superalias (sv::name-fix name) width lsb) (vlsv-aggregate-superalias name width lsb)))
Theorem:
(defthm vlsv-aggregate-superalias-name-equiv-congruence-on-name (implies (sv::name-equiv name name-equiv) (equal (vlsv-aggregate-superalias name width lsb) (vlsv-aggregate-superalias name-equiv width lsb))) :rule-classes :congruence)
Theorem:
(defthm vlsv-aggregate-superalias-of-pos-fix-width (equal (vlsv-aggregate-superalias name (pos-fix width) lsb) (vlsv-aggregate-superalias name width lsb)))
Theorem:
(defthm vlsv-aggregate-superalias-pos-equiv-congruence-on-width (implies (acl2::pos-equiv width width-equiv) (equal (vlsv-aggregate-superalias name width lsb) (vlsv-aggregate-superalias name width-equiv lsb))) :rule-classes :congruence)
Theorem:
(defthm vlsv-aggregate-superalias-of-nfix-lsb (equal (vlsv-aggregate-superalias name width (nfix lsb)) (vlsv-aggregate-superalias name width lsb)))
Theorem:
(defthm vlsv-aggregate-superalias-nat-equiv-congruence-on-lsb (implies (acl2::nat-equiv lsb lsb-equiv) (equal (vlsv-aggregate-superalias name width lsb) (vlsv-aggregate-superalias name width lsb-equiv))) :rule-classes :congruence)