Function:
(defun s4vec-bit?! (test thens elses) (declare (xargs :guard (and (s4vec-p test) (s4vec-p thens) (s4vec-p elses)))) (let ((__function__ 's4vec-bit?!)) (declare (ignorable __function__)) (s4vec-bitmux (s4vec-1mask test) thens elses)))
Theorem:
(defthm s4vec-p-of-s4vec-bit?! (b* ((res (s4vec-bit?! test thens elses))) (s4vec-p res)) :rule-classes :rewrite)
Theorem:
(defthm s4vec-bit?!-correct (b* ((?res (s4vec-bit?! test thens elses))) (equal (s4vec->4vec res) (4vec-bit?! (s4vec->4vec test) (s4vec->4vec thens) (s4vec->4vec elses)))))
Theorem:
(defthm s4vec-bit?!-of-s4vec-fix-test (equal (s4vec-bit?! (s4vec-fix test) thens elses) (s4vec-bit?! test thens elses)))
Theorem:
(defthm s4vec-bit?!-s4vec-equiv-congruence-on-test (implies (s4vec-equiv test test-equiv) (equal (s4vec-bit?! test thens elses) (s4vec-bit?! test-equiv thens elses))) :rule-classes :congruence)
Theorem:
(defthm s4vec-bit?!-of-s4vec-fix-thens (equal (s4vec-bit?! test (s4vec-fix thens) elses) (s4vec-bit?! test thens elses)))
Theorem:
(defthm s4vec-bit?!-s4vec-equiv-congruence-on-thens (implies (s4vec-equiv thens thens-equiv) (equal (s4vec-bit?! test thens elses) (s4vec-bit?! test thens-equiv elses))) :rule-classes :congruence)
Theorem:
(defthm s4vec-bit?!-of-s4vec-fix-elses (equal (s4vec-bit?! test thens (s4vec-fix elses)) (s4vec-bit?! test thens elses)))
Theorem:
(defthm s4vec-bit?!-s4vec-equiv-congruence-on-elses (implies (s4vec-equiv elses elses-equiv) (equal (s4vec-bit?! test thens elses) (s4vec-bit?! test thens elses-equiv))) :rule-classes :congruence)