(vl-case-conservative-test-expr test full-conservative part-conservative) → full-test
Function:
(defun vl-case-conservative-test-expr (test full-conservative part-conservative) (declare (xargs :guard (and (sv::svex-p test) (sv::svex-p full-conservative) (sv::svex-p part-conservative)))) (let ((__function__ 'vl-case-conservative-test-expr)) (declare (ignorable __function__)) (b* ((multi-test (if (equal (sv::svex-fix part-conservative) 0) (sv::svex-fix test) (sv::svcall sv::bitand test (sv::svcall sv::? part-conservative (sv::svex-x) 1)))) (none-test (if (equal (sv::svex-fix full-conservative) 0) multi-test (sv::svcall sv::? full-conservative (sv::svex-x) multi-test)))) none-test)))
Theorem:
(defthm svex-p-of-vl-case-conservative-test-expr (b* ((full-test (vl-case-conservative-test-expr test full-conservative part-conservative))) (sv::svex-p full-test)) :rule-classes :rewrite)
Theorem:
(defthm svex-addr-p-of-vl-case-conservative-test-expr (b* ((?full-test (vl-case-conservative-test-expr test full-conservative part-conservative))) (implies (and (sv::svarlist-addr-p (sv::svex-vars test)) (sv::svarlist-addr-p (sv::svex-vars full-conservative)) (sv::svarlist-addr-p (sv::svex-vars part-conservative))) (sv::svarlist-addr-p (sv::svex-vars full-test)))))
Theorem:
(defthm vl-case-conservative-test-expr-of-svex-fix-test (equal (vl-case-conservative-test-expr (sv::svex-fix test) full-conservative part-conservative) (vl-case-conservative-test-expr test full-conservative part-conservative)))
Theorem:
(defthm vl-case-conservative-test-expr-svex-equiv-congruence-on-test (implies (sv::svex-equiv test test-equiv) (equal (vl-case-conservative-test-expr test full-conservative part-conservative) (vl-case-conservative-test-expr test-equiv full-conservative part-conservative))) :rule-classes :congruence)
Theorem:
(defthm vl-case-conservative-test-expr-of-svex-fix-full-conservative (equal (vl-case-conservative-test-expr test (sv::svex-fix full-conservative) part-conservative) (vl-case-conservative-test-expr test full-conservative part-conservative)))
Theorem:
(defthm vl-case-conservative-test-expr-svex-equiv-congruence-on-full-conservative (implies (sv::svex-equiv full-conservative full-conservative-equiv) (equal (vl-case-conservative-test-expr test full-conservative part-conservative) (vl-case-conservative-test-expr test full-conservative-equiv part-conservative))) :rule-classes :congruence)
Theorem:
(defthm vl-case-conservative-test-expr-of-svex-fix-part-conservative (equal (vl-case-conservative-test-expr test full-conservative (sv::svex-fix part-conservative)) (vl-case-conservative-test-expr test full-conservative part-conservative)))
Theorem:
(defthm vl-case-conservative-test-expr-svex-equiv-congruence-on-part-conservative (implies (sv::svex-equiv part-conservative part-conservative-equiv) (equal (vl-case-conservative-test-expr test full-conservative part-conservative) (vl-case-conservative-test-expr test full-conservative part-conservative-equiv))) :rule-classes :congruence)