(vl-caseexprs->svex-test x test size casetype casekey ss scopes) → (mv vttree cond)
Function:
(defun vl-caseexprs->svex-test (x test size casetype casekey ss scopes) (declare (xargs :guard (and (vl-exprlist-p x) (sv::svex-p test) (natp size) (vl-casetype-p casetype) (vl-casekey-p casekey) (vl-scopestack-p ss) (vl-elabscopes-p scopes)))) (let ((__function__ 'vl-caseexprs->svex-test)) (declare (ignorable __function__)) (if (atom x) (mv nil (svex-int 0)) (b* (((mv vttree rest) (vl-caseexprs->svex-test (cdr x) test size casetype casekey ss scopes)) ((vmv vttree first &) (vl-expr-to-svex-selfdet (car x) (lnfix size) ss scopes))) (mv vttree (sv::svcall sv::bitor (if (or (vl-casetype-fix casetype) (vl-casekey-fix casekey)) (sv::svcall sv::==?? test first) (sv::svcall sv::== test first)) rest))))))
Theorem:
(defthm return-type-of-vl-caseexprs->svex-test.vttree (b* (((mv ?vttree common-lisp::?cond) (vl-caseexprs->svex-test x test size casetype casekey ss scopes))) (and (vttree-p vttree) (sv::svarlist-addr-p (sv::constraintlist-vars (vttree->constraints vttree))))) :rule-classes :rewrite)
Theorem:
(defthm svex-p-of-vl-caseexprs->svex-test.cond (b* (((mv ?vttree common-lisp::?cond) (vl-caseexprs->svex-test x test size casetype casekey ss scopes))) (sv::svex-p cond)) :rule-classes :rewrite)
Theorem:
(defthm vars-of-vl-caseexprs->svex-test (b* (((mv ?vttree common-lisp::?cond) (vl-caseexprs->svex-test x test size casetype casekey ss scopes))) (implies (sv::svarlist-addr-p (sv::svex-vars test)) (sv::svarlist-addr-p (sv::svex-vars cond)))))
Theorem:
(defthm vl-caseexprs->svex-test-of-vl-exprlist-fix-x (equal (vl-caseexprs->svex-test (vl-exprlist-fix x) test size casetype casekey ss scopes) (vl-caseexprs->svex-test x test size casetype casekey ss scopes)))
Theorem:
(defthm vl-caseexprs->svex-test-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-caseexprs->svex-test x test size casetype casekey ss scopes) (vl-caseexprs->svex-test x-equiv test size casetype casekey ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-caseexprs->svex-test-of-svex-fix-test (equal (vl-caseexprs->svex-test x (sv::svex-fix test) size casetype casekey ss scopes) (vl-caseexprs->svex-test x test size casetype casekey ss scopes)))
Theorem:
(defthm vl-caseexprs->svex-test-svex-equiv-congruence-on-test (implies (sv::svex-equiv test test-equiv) (equal (vl-caseexprs->svex-test x test size casetype casekey ss scopes) (vl-caseexprs->svex-test x test-equiv size casetype casekey ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-caseexprs->svex-test-of-nfix-size (equal (vl-caseexprs->svex-test x test (nfix size) casetype casekey ss scopes) (vl-caseexprs->svex-test x test size casetype casekey ss scopes)))
Theorem:
(defthm vl-caseexprs->svex-test-nat-equiv-congruence-on-size (implies (acl2::nat-equiv size size-equiv) (equal (vl-caseexprs->svex-test x test size casetype casekey ss scopes) (vl-caseexprs->svex-test x test size-equiv casetype casekey ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-caseexprs->svex-test-of-vl-casetype-fix-casetype (equal (vl-caseexprs->svex-test x test size (vl-casetype-fix casetype) casekey ss scopes) (vl-caseexprs->svex-test x test size casetype casekey ss scopes)))
Theorem:
(defthm vl-caseexprs->svex-test-vl-casetype-equiv-congruence-on-casetype (implies (vl-casetype-equiv casetype casetype-equiv) (equal (vl-caseexprs->svex-test x test size casetype casekey ss scopes) (vl-caseexprs->svex-test x test size casetype-equiv casekey ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-caseexprs->svex-test-of-vl-casekey-fix-casekey (equal (vl-caseexprs->svex-test x test size casetype (vl-casekey-fix casekey) ss scopes) (vl-caseexprs->svex-test x test size casetype casekey ss scopes)))
Theorem:
(defthm vl-caseexprs->svex-test-vl-casekey-equiv-congruence-on-casekey (implies (vl-casekey-equiv casekey casekey-equiv) (equal (vl-caseexprs->svex-test x test size casetype casekey ss scopes) (vl-caseexprs->svex-test x test size casetype casekey-equiv ss scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-caseexprs->svex-test-of-vl-scopestack-fix-ss (equal (vl-caseexprs->svex-test x test size casetype casekey (vl-scopestack-fix ss) scopes) (vl-caseexprs->svex-test x test size casetype casekey ss scopes)))
Theorem:
(defthm vl-caseexprs->svex-test-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-caseexprs->svex-test x test size casetype casekey ss scopes) (vl-caseexprs->svex-test x test size casetype casekey ss-equiv scopes))) :rule-classes :congruence)
Theorem:
(defthm vl-caseexprs->svex-test-of-vl-elabscopes-fix-scopes (equal (vl-caseexprs->svex-test x test size casetype casekey ss (vl-elabscopes-fix scopes)) (vl-caseexprs->svex-test x test size casetype casekey ss scopes)))
Theorem:
(defthm vl-caseexprs->svex-test-vl-elabscopes-equiv-congruence-on-scopes (implies (vl-elabscopes-equiv scopes scopes-equiv) (equal (vl-caseexprs->svex-test x test size casetype casekey ss scopes) (vl-caseexprs->svex-test x test size casetype casekey ss scopes-equiv))) :rule-classes :congruence)