(vl-elim-nested-concats-pass x) → (mv progressp new-x)
Function:
(defun vl-elim-nested-concats-pass (x) (declare (xargs :guard (vl-exprlist-p x))) (let ((__function__ 'vl-elim-nested-concats-pass)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv cdr-progressp cdr-prime) (vl-elim-nested-concats-pass (cdr x))) (expr1 (vl-expr-fix (car x))) ((unless (and (not (vl-fast-atom-p expr1)) (eq (vl-nonatom->op expr1) :vl-concat))) (mv cdr-progressp (cons expr1 cdr-prime))) (args (vl-nonatom->args expr1))) (mv t (append-without-guard args cdr-prime)))))
Theorem:
(defthm booleanp-of-vl-elim-nested-concats-pass.progressp (b* (((mv ?progressp ?new-x) (vl-elim-nested-concats-pass x))) (booleanp progressp)) :rule-classes :type-prescription)
Theorem:
(defthm vl-exprlist-p-of-vl-elim-nested-concats-pass.new-x (b* (((mv ?progressp ?new-x) (vl-elim-nested-concats-pass x))) (vl-exprlist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm vl-elim-nested-concats-pass-mvtypes-1 (true-listp (mv-nth 1 (vl-elim-nested-concats-pass x))) :rule-classes :type-prescription)
Theorem:
(defthm vl-exprlist-count-of-vl-elim-nested-concats-pass-weak (<= (vl-exprlist-count (mv-nth 1 (vl-elim-nested-concats-pass x))) (vl-exprlist-count x)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-exprlist-count-of-vl-elim-nested-concats-pass-strong (implies (mv-nth 0 (vl-elim-nested-concats-pass x)) (< (vl-exprlist-count (mv-nth 1 (vl-elim-nested-concats-pass x))) (vl-exprlist-count x))) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm vl-elim-nested-concats-pass-of-vl-exprlist-fix-x (equal (vl-elim-nested-concats-pass (vl-exprlist-fix x)) (vl-elim-nested-concats-pass x)))
Theorem:
(defthm vl-elim-nested-concats-pass-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-elim-nested-concats-pass x) (vl-elim-nested-concats-pass x-equiv))) :rule-classes :congruence)