(svexlist-normalize-concats x &key (verbosep 'nil)) → new-x
Function:
(defun svexlist-normalize-concats-fn (x verbosep) (declare (xargs :guard (svexlist-p x))) (let ((__function__ 'svexlist-normalize-concats)) (declare (ignorable __function__)) (b* ((- (and verbosep (cw "opcount before norm-concats: ~x0~%" (svexlist-opcount x)))) (ctxalist (time$ (svexlist-make-top-context-alist x nil) :mintime 1 :msg "; norm-concats: context alist: ~st sec, ~sa bytes~%")) (res (time$ (svexlist-normalize-concats-aux x ctxalist) :mintime 1 :msg "; norm-concats main: ~st sec, ~sa bytes~%"))) (clear-memoize-table 'svex-normalize-concats-aux) (fast-alist-free ctxalist) (and verbosep (cw "opcount after norm-concats: ~x0~%" (svexlist-opcount res))) res)))
Theorem:
(defthm return-type-of-svexlist-normalize-concats (b* ((new-x (svexlist-normalize-concats-fn x verbosep))) (and (svexlist-p new-x) (equal (len new-x) (len x)))) :rule-classes :rewrite)
Theorem:
(defthm svexlist-normalize-concats-correct (b* ((?new-x (svexlist-normalize-concats-fn x verbosep))) (equal (svexlist-eval new-x env) (svexlist-eval x env))))
Theorem:
(defthm vars-of-svexlist-normalize-concats (b* ((?new-x (svexlist-normalize-concats-fn x verbosep))) (implies (not (member v (svexlist-vars x))) (not (member v (svexlist-vars new-x))))))
Theorem:
(defthm svexlist-normalize-concats-fn-of-svexlist-fix-x (equal (svexlist-normalize-concats-fn (svexlist-fix x) verbosep) (svexlist-normalize-concats-fn x verbosep)))
Theorem:
(defthm svexlist-normalize-concats-fn-svexlist-equiv-congruence-on-x (implies (svexlist-equiv x x-equiv) (equal (svexlist-normalize-concats-fn x verbosep) (svexlist-normalize-concats-fn x-equiv verbosep))) :rule-classes :congruence)