(envmap-to-term-alist x) → xal
Function:
(defun envmap-to-term-alist (x) (declare (xargs :guard (envmap-p x))) (let ((__function__ 'envmap-to-term-alist)) (declare (ignorable __function__)) (if (atom x) nil (if (mbt (consp (car x))) (append (envmap-entry-to-term-alist (cdar x) (caar x)) (envmap-to-term-alist (cdr x))) (envmap-to-term-alist (cdr x))))))
Theorem:
(defthm return-type-of-envmap-to-term-alist (b* ((xal (envmap-to-term-alist x))) (and (implies (envmap-p x) (svdecomp-symenv-p xal)) (svar-alist-p xal))) :rule-classes :rewrite)
Theorem:
(defthm eval-of-envmap-to-term-alist (equal (svdecomp-ev-symenv (envmap-to-term-alist x) a) (svdecomp-ev-envmap x a)))
Theorem:
(defthm envmap-to-term-alist-of-append (equal (envmap-to-term-alist (append a b)) (append (envmap-to-term-alist a) (envmap-to-term-alist b))))
Theorem:
(defthm envmap-to-term-alist-of-svex-alist-alist-fix-x (equal (envmap-to-term-alist (svex-alist-alist-fix x)) (envmap-to-term-alist x)))
Theorem:
(defthm envmap-to-term-alist-svex-alist-alist-equiv-congruence-on-x (implies (svex-alist-alist-equiv x x-equiv) (equal (envmap-to-term-alist x) (envmap-to-term-alist x-equiv))) :rule-classes :congruence)