(vl-casezx-elim-aux type test cases default ctx warnings) → (mv warnings new-stmt?)
Function:
(defun vl-casezx-elim-aux (type test cases default ctx warnings) (declare (xargs :guard (and (vl-casetype-p type) (vl-expr-p test) (vl-caselist-p cases) (vl-stmt-p default) (vl-modelement-p ctx) (vl-warninglist-p warnings)))) (declare (xargs :guard (and (member type '(:vl-casez :vl-casex)) (vl-expr-welltyped-p test) (posp (vl-expr->finalwidth test)) (equal (vl-expr->finaltype test) :vl-unsigned)))) (let ((__function__ 'vl-casezx-elim-aux)) (declare (ignorable __function__)) (b* ((cases (vl-caselist-fix cases)) (default (vl-stmt-fix default)) ((when (atom cases)) (mv (ok) default)) ((cons match-exprs1 body1) (car cases)) ((mv warnings match-expr) (vl-casezx-match-any-expr type test match-exprs1 ctx warnings)) ((unless match-expr) (mv warnings nil)) ((mv warnings rest-stmt) (vl-casezx-elim-aux type test (cdr cases) default ctx warnings)) ((unless rest-stmt) (mv warnings nil)) (new-stmt (make-vl-ifstmt :condition match-expr :truebranch body1 :falsebranch rest-stmt))) (mv warnings new-stmt))))
Theorem:
(defthm vl-warninglist-p-of-vl-casezx-elim-aux.warnings (b* (((mv ?warnings ?new-stmt?) (vl-casezx-elim-aux type test cases default ctx warnings))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-casezx-elim-aux.new-stmt? (b* (((mv ?warnings ?new-stmt?) (vl-casezx-elim-aux type test cases default ctx warnings))) (equal (vl-stmt-p new-stmt?) (if new-stmt? t nil))) :rule-classes :rewrite)
Theorem:
(defthm vl-casezx-elim-aux-of-vl-casetype-fix-type (equal (vl-casezx-elim-aux (vl-casetype-fix type) test cases default ctx warnings) (vl-casezx-elim-aux type test cases default ctx warnings)))
Theorem:
(defthm vl-casezx-elim-aux-vl-casetype-equiv-congruence-on-type (implies (vl-casetype-equiv type type-equiv) (equal (vl-casezx-elim-aux type test cases default ctx warnings) (vl-casezx-elim-aux type-equiv test cases default ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-elim-aux-of-vl-expr-fix-test (equal (vl-casezx-elim-aux type (vl-expr-fix test) cases default ctx warnings) (vl-casezx-elim-aux type test cases default ctx warnings)))
Theorem:
(defthm vl-casezx-elim-aux-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casezx-elim-aux type test cases default ctx warnings) (vl-casezx-elim-aux type test-equiv cases default ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-elim-aux-of-vl-caselist-fix-cases (equal (vl-casezx-elim-aux type test (vl-caselist-fix cases) default ctx warnings) (vl-casezx-elim-aux type test cases default ctx warnings)))
Theorem:
(defthm vl-casezx-elim-aux-vl-caselist-equiv-congruence-on-cases (implies (vl-caselist-equiv cases cases-equiv) (equal (vl-casezx-elim-aux type test cases default ctx warnings) (vl-casezx-elim-aux type test cases-equiv default ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-elim-aux-of-vl-stmt-fix-default (equal (vl-casezx-elim-aux type test cases (vl-stmt-fix default) ctx warnings) (vl-casezx-elim-aux type test cases default ctx warnings)))
Theorem:
(defthm vl-casezx-elim-aux-vl-stmt-equiv-congruence-on-default (implies (vl-stmt-equiv default default-equiv) (equal (vl-casezx-elim-aux type test cases default ctx warnings) (vl-casezx-elim-aux type test cases default-equiv ctx warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-elim-aux-of-vl-modelement-fix-ctx (equal (vl-casezx-elim-aux type test cases default (vl-modelement-fix ctx) warnings) (vl-casezx-elim-aux type test cases default ctx warnings)))
Theorem:
(defthm vl-casezx-elim-aux-vl-modelement-equiv-congruence-on-ctx (implies (vl-modelement-equiv ctx ctx-equiv) (equal (vl-casezx-elim-aux type test cases default ctx warnings) (vl-casezx-elim-aux type test cases default ctx-equiv warnings))) :rule-classes :congruence)
Theorem:
(defthm vl-casezx-elim-aux-of-vl-warninglist-fix-warnings (equal (vl-casezx-elim-aux type test cases default ctx (vl-warninglist-fix warnings)) (vl-casezx-elim-aux type test cases default ctx warnings)))
Theorem:
(defthm vl-casezx-elim-aux-vl-warninglist-equiv-congruence-on-warnings (implies (vl-warninglist-equiv warnings warnings-equiv) (equal (vl-casezx-elim-aux type test cases default ctx warnings) (vl-casezx-elim-aux type test cases default ctx warnings-equiv))) :rule-classes :congruence)