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