(svex-alist-eval-aux x env) → xx
Function:
(defun svex-alist-eval-aux (x env) (declare (xargs :guard (and (svex-alist-p x) (svex-env-p env)))) (let ((__function__ 'svex-alist-eval-aux)) (declare (ignorable __function__)) (if (atom x) nil (if (mbt (and (consp (car x)) (svar-p (caar x)))) (cons (cons (caar x) (svex-eval (cdar x) env)) (svex-alist-eval-aux (cdr x) env)) (svex-alist-eval-aux (cdr x) env)))))
Theorem:
(defthm svex-env-p-of-svex-alist-eval-aux (b* ((xx (svex-alist-eval-aux x env))) (svex-env-p xx)) :rule-classes :rewrite)