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