(svex-alist-normalize-concats x &key (verbosep 'nil)) → new-x
Function:
(defun svex-alist-normalize-concats-fn (x verbosep) (declare (xargs :guard (svex-alist-p x))) (let ((__function__ 'svex-alist-normalize-concats)) (declare (ignorable __function__)) (pairlis$ (svex-alist-keys x) (svexlist-normalize-concats (svex-alist-vals x) :verbosep verbosep))))
Theorem:
(defthm svex-alist-p-of-svex-alist-normalize-concats (b* ((new-x (svex-alist-normalize-concats-fn x verbosep))) (svex-alist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm svex-alist-normalize-concats-fn-of-svex-alist-fix-x (equal (svex-alist-normalize-concats-fn (svex-alist-fix x) verbosep) (svex-alist-normalize-concats-fn x verbosep)))
Theorem:
(defthm svex-alist-normalize-concats-fn-svex-alist-equiv-congruence-on-x (implies (svex-alist-equiv x x-equiv) (equal (svex-alist-normalize-concats-fn x verbosep) (svex-alist-normalize-concats-fn x-equiv verbosep))) :rule-classes :congruence)
Theorem:
(defthm svex-alist-normalize-concats-correct (equal (svex-alist-eval (svex-alist-normalize-concats x :verbosep verbosep) env) (svex-alist-eval x env)))
Theorem:
(defthm len-of-svex-alist-normalize-concats (equal (len (svex-alist-normalize-concats x :verbosep verbosep)) (len (svex-alist-fix x))))
Theorem:
(defthm svex-lookup-in-pairlis$ (implies (equal (len x) (len y)) (iff (svex-lookup v (pairlis$ x y)) (member (svar-fix v) x))))
Theorem:
(defthm vars-of-svex-alist-normalize-concats (implies (not (member v (svex-alist-vars x))) (not (member v (svex-alist-vars (svex-alist-normalize-concats x :verbosep verbosep))))))
Theorem:
(defthm keys-of-svex-alist-normalize-concats (iff (svex-lookup v (svex-alist-normalize-concats x :verbosep verbosep)) (svex-lookup v x)))
Theorem:
(defthm svex-alist-keys-of-svex-alist-normalize-concats (b* ((?new-x (svex-alist-normalize-concats-fn x verbosep))) (equal (svex-alist-keys new-x) (svex-alist-keys x))))