(vl-case-xcond-wrapper x full-conservative config) → new-x
Function:
(defun vl-case-xcond-wrapper (x full-conservative config) (declare (xargs :guard (and (sv::svstmtlist-p x) (sv::svex-p full-conservative) (svstmt-config-p config)))) (let ((__function__ 'vl-case-xcond-wrapper)) (declare (ignorable __function__)) (b* ((conservative (svstmt-config->uniquecase-conservative config)) ((unless (and (<= 3 (lnfix conservative)) (not (equal (sv::svex-fix full-conservative) 0)))) (sv::svstmtlist-fix x))) (list (sv::make-svstmt-xcond :cond full-conservative :body x)))))
Theorem:
(defthm svstmtlist-p-of-vl-case-xcond-wrapper (b* ((new-x (vl-case-xcond-wrapper x full-conservative config))) (sv::svstmtlist-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm svarlist-addr-p-of-vl-case-xcond-wrapper (b* ((?new-x (vl-case-xcond-wrapper x full-conservative config))) (implies (and (sv::svarlist-addr-p (sv::svex-vars full-conservative)) (sv::svarlist-addr-p (sv::svstmtlist-vars x))) (sv::svarlist-addr-p (sv::svstmtlist-vars new-x)))))
Theorem:
(defthm vl-case-xcond-wrapper-of-svstmtlist-fix-x (equal (vl-case-xcond-wrapper (sv::svstmtlist-fix x) full-conservative config) (vl-case-xcond-wrapper x full-conservative config)))
Theorem:
(defthm vl-case-xcond-wrapper-svstmtlist-equiv-congruence-on-x (implies (sv::svstmtlist-equiv x x-equiv) (equal (vl-case-xcond-wrapper x full-conservative config) (vl-case-xcond-wrapper x-equiv full-conservative config))) :rule-classes :congruence)
Theorem:
(defthm vl-case-xcond-wrapper-of-svex-fix-full-conservative (equal (vl-case-xcond-wrapper x (sv::svex-fix full-conservative) config) (vl-case-xcond-wrapper x full-conservative config)))
Theorem:
(defthm vl-case-xcond-wrapper-svex-equiv-congruence-on-full-conservative (implies (sv::svex-equiv full-conservative full-conservative-equiv) (equal (vl-case-xcond-wrapper x full-conservative config) (vl-case-xcond-wrapper x full-conservative-equiv config))) :rule-classes :congruence)
Theorem:
(defthm vl-case-xcond-wrapper-of-svstmt-config-fix-config (equal (vl-case-xcond-wrapper x full-conservative (svstmt-config-fix config)) (vl-case-xcond-wrapper x full-conservative config)))
Theorem:
(defthm vl-case-xcond-wrapper-svstmt-config-equiv-congruence-on-config (implies (svstmt-config-equiv config config-equiv) (equal (vl-case-xcond-wrapper x full-conservative config) (vl-case-xcond-wrapper x full-conservative config-equiv))) :rule-classes :congruence)