(svex-lhses-from-names x) → lhses
Function:
(defun svex-lhses-from-names (x) (declare (xargs :guard (string-listp x))) (let ((__function__ 'svex-lhses-from-names)) (declare (ignorable __function__)) (if (atom x) nil (cons (svex-lhs-from-name (car x)) (svex-lhses-from-names (cdr x))))))
Theorem:
(defthm lhslist-p-of-svex-lhses-from-names (b* ((lhses (svex-lhses-from-names x))) (sv::lhslist-p lhses)) :rule-classes :rewrite)
Theorem:
(defthm len-of-svex-lhses-from-names (b* ((?lhses (svex-lhses-from-names x))) (equal (len lhses) (len x))))
Theorem:
(defthm svarlist-addr-p-of-svex-lhses-from-names (b* ((?lhses (svex-lhses-from-names x))) (sv::svarlist-addr-p (sv::lhslist-vars lhses))))
Theorem:
(defthm svex-lhses-from-names-of-string-list-fix-x (equal (svex-lhses-from-names (string-list-fix x)) (svex-lhses-from-names x)))
Theorem:
(defthm svex-lhses-from-names-string-list-equiv-congruence-on-x (implies (str::string-list-equiv x x-equiv) (equal (svex-lhses-from-names x) (svex-lhses-from-names x-equiv))) :rule-classes :congruence)