(svstack-to-svex-alist x) → x-alist
Function:
(defun svstack-to-svex-alist (x) (declare (xargs :guard (svstack-p x))) (let ((__function__ 'svstack-to-svex-alist)) (declare (ignorable __function__)) (if (atom x) nil (append (svex-alist-fix (car x)) (svstack-to-svex-alist (cdr x))))))
Theorem:
(defthm svex-alist-p-of-svstack-to-svex-alist (b* ((x-alist (svstack-to-svex-alist x))) (svex-alist-p x-alist)) :rule-classes :rewrite)
Theorem:
(defthm svex-lookup-of-svstack-to-svex-alist-cons (equal (svex-lookup k (svstack-to-svex-alist (cons a b))) (or (svex-lookup k a) (svex-lookup k (svstack-to-svex-alist b)))))
Theorem:
(defthm svex-lookup-of-svstack-to-svex-alist-consp (implies (consp x) (equal (svex-lookup k (svstack-to-svex-alist x)) (or (svex-lookup k (car x)) (svex-lookup k (svstack-to-svex-alist (cdr x)))))))
Theorem:
(defthm svex-vars-of-svstack-to-svex-alist-cons (set-equiv (svex-alist-vars (svstack-to-svex-alist (cons a b))) (append (svex-alist-vars a) (svex-alist-vars (svstack-to-svex-alist b)))))
Theorem:
(defthm svstack-to-svex-alist-when-atom (implies (atom x) (equal (svstack-to-svex-alist x) nil)) :rule-classes ((:rewrite :backchain-limit-lst 0)))
Theorem:
(defthm svstack-to-svex-alist-of-svstack-fix-x (equal (svstack-to-svex-alist (svstack-fix x)) (svstack-to-svex-alist x)))
Theorem:
(defthm svstack-to-svex-alist-svstack-equiv-congruence-on-x (implies (svstack-equiv x x-equiv) (equal (svstack-to-svex-alist x) (svstack-to-svex-alist x-equiv))) :rule-classes :congruence)