Function:
(defun svex-lhs-from-name-fn (name width rsh) (declare (xargs :guard (and (stringp name) (posp width) (natp rsh)))) (let ((__function__ 'svex-lhs-from-name)) (declare (ignorable __function__)) (list (sv::make-lhrange :w width :atom (sv::make-lhatom-var :name (svex-svar-from-name name) :rsh rsh)))))
Theorem:
(defthm lhs-p-of-svex-lhs-from-name (b* ((lhs (svex-lhs-from-name-fn name width rsh))) (sv::lhs-p lhs)) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-of-svex-lhs-from-name (b* ((?lhs (svex-lhs-from-name-fn name width rsh))) (sv::svarlist-addr-p (sv::lhs-vars lhs))))
Theorem:
(defthm svex-lhs-from-name-fn-of-str-fix-name (equal (svex-lhs-from-name-fn (str-fix name) width rsh) (svex-lhs-from-name-fn name width rsh)))
Theorem:
(defthm svex-lhs-from-name-fn-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (svex-lhs-from-name-fn name width rsh) (svex-lhs-from-name-fn name-equiv width rsh))) :rule-classes :congruence)
Theorem:
(defthm svex-lhs-from-name-fn-of-pos-fix-width (equal (svex-lhs-from-name-fn name (pos-fix width) rsh) (svex-lhs-from-name-fn name width rsh)))
Theorem:
(defthm svex-lhs-from-name-fn-pos-equiv-congruence-on-width (implies (acl2::pos-equiv width width-equiv) (equal (svex-lhs-from-name-fn name width rsh) (svex-lhs-from-name-fn name width-equiv rsh))) :rule-classes :congruence)
Theorem:
(defthm svex-lhs-from-name-fn-of-nfix-rsh (equal (svex-lhs-from-name-fn name width (nfix rsh)) (svex-lhs-from-name-fn name width rsh)))
Theorem:
(defthm svex-lhs-from-name-fn-nat-equiv-congruence-on-rsh (implies (acl2::nat-equiv rsh rsh-equiv) (equal (svex-lhs-from-name-fn name width rsh) (svex-lhs-from-name-fn name width rsh-equiv))) :rule-classes :congruence)