(envmap->svex-alist envmap) → svalist
Function:
(defun envmap->svex-alist (envmap) (declare (xargs :guard (envmap-p envmap))) (let ((__function__ 'envmap->svex-alist)) (declare (ignorable __function__)) (if (atom envmap) nil (if (mbt (consp (car envmap))) (append (svex-alist-fix (cdar envmap)) (envmap->svex-alist (cdr envmap))) (envmap->svex-alist (cdr envmap))))))
Theorem:
(defthm svex-alist-p-of-envmap->svex-alist (b* ((svalist (envmap->svex-alist envmap))) (svex-alist-p svalist)) :rule-classes :rewrite)
Theorem:
(defthm envmap->svex-alist-of-append (equal (envmap->svex-alist (append a b)) (append (envmap->svex-alist a) (envmap->svex-alist b))))
Theorem:
(defthm envmap->svex-alist-of-atom (implies (not (consp envmap)) (equal (envmap->svex-alist envmap) nil)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm svar-lookup-of-envmap-to-term-alist-under-iff (iff (svar-lookup k (envmap-to-term-alist x)) (svar-lookup k (envmap->svex-alist x))))
Theorem:
(defthm envmap->svex-alist-of-svex-alist-alist-fix-envmap (equal (envmap->svex-alist (svex-alist-alist-fix envmap)) (envmap->svex-alist envmap)))
Theorem:
(defthm envmap->svex-alist-svex-alist-alist-equiv-congruence-on-envmap (implies (svex-alist-alist-equiv envmap envmap-equiv) (equal (envmap->svex-alist envmap) (envmap->svex-alist envmap-equiv))) :rule-classes :congruence)