(map-alist-const-keys-to-val-terms x) → res
Function:
(defun map-alist-const-keys-to-val-terms (x) (declare (xargs :guard (svex-env-p x))) (let ((__function__ 'map-alist-const-keys-to-val-terms)) (declare (ignorable __function__)) (if (atom x) nil (if (mbt (and (consp (car x)) (svar-p (caar x)))) (cons (cons (caar x) (list 'quote (4vec-fix (cdar x)))) (map-alist-const-keys-to-val-terms (cdr x))) (map-alist-const-keys-to-val-terms (cdr x))))))
Theorem:
(defthm svdecomp-symenv-p-of-map-alist-const-keys-to-val-terms (b* ((res (map-alist-const-keys-to-val-terms x))) (svdecomp-symenv-p res)) :rule-classes :rewrite)
Theorem:
(defthm eval-lookup-of-map-alist-const-keys-to-val-terms (let ((al (map-alist-const-keys-to-val-terms x))) (implies (svar-lookup k (svex-env-fix x)) (equal (svdecomp-ev (cdr (svar-lookup k al)) env) (cdr (svar-lookup k (svex-env-fix x)))))))
Theorem:
(defthm lookup-exists-of-map-alist-const-keys-to-val-terms (iff (svar-lookup k (map-alist-const-keys-to-val-terms x)) (svar-lookup k (svex-env-fix x))))
Theorem:
(defthm svdecomp-ev-symenv-of-map-alist-const-keys-to-val-terms (equal (svdecomp-ev-symenv (map-alist-const-keys-to-val-terms x) env) (svex-env-fix x)))
Theorem:
(defthm map-alist-const-keys-to-val-terms-of-svex-env-fix-x (equal (map-alist-const-keys-to-val-terms (svex-env-fix x)) (map-alist-const-keys-to-val-terms x)))
Theorem:
(defthm map-alist-const-keys-to-val-terms-svex-env-equiv-congruence-on-x (implies (svex-env-equiv x x-equiv) (equal (map-alist-const-keys-to-val-terms x) (map-alist-const-keys-to-val-terms x-equiv))) :rule-classes :congruence)