Update the |FGL|::|MAKE-ITES| field of a interp-flags bit structure.
(!interp-flags->make-ites make-ites x) → new-x
Function:
(defun !interp-flags->make-ites (make-ites x) (declare (xargs :guard (and (booleanp make-ites) (interp-flags-p x)))) (mbe :logic (b* ((make-ites (bool->bit make-ites)) (x (interp-flags-fix x))) (acl2::part-install make-ites x :width 1 :low 4)) :exec (the (unsigned-byte 6) (logior (the (unsigned-byte 6) (logand (the (unsigned-byte 6) x) (the (signed-byte 6) -17))) (the (unsigned-byte 5) (ash (the (unsigned-byte 1) (bool->bit make-ites)) 4))))))
Theorem:
(defthm interp-flags-p-of-!interp-flags->make-ites (b* ((new-x (!interp-flags->make-ites make-ites x))) (interp-flags-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !interp-flags->make-ites-of-bool-fix-make-ites (equal (!interp-flags->make-ites (bool-fix make-ites) x) (!interp-flags->make-ites make-ites x)))
Theorem:
(defthm !interp-flags->make-ites-iff-congruence-on-make-ites (implies (iff make-ites make-ites-equiv) (equal (!interp-flags->make-ites make-ites x) (!interp-flags->make-ites make-ites-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->make-ites-of-interp-flags-fix-x (equal (!interp-flags->make-ites make-ites (interp-flags-fix x)) (!interp-flags->make-ites make-ites x)))
Theorem:
(defthm !interp-flags->make-ites-interp-flags-equiv-congruence-on-x (implies (interp-flags-equiv x x-equiv) (equal (!interp-flags->make-ites make-ites x) (!interp-flags->make-ites make-ites x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !interp-flags->make-ites-is-interp-flags (equal (!interp-flags->make-ites make-ites x) (change-interp-flags x :make-ites make-ites)))
Theorem:
(defthm interp-flags->make-ites-of-!interp-flags->make-ites (b* ((?new-x (!interp-flags->make-ites make-ites x))) (equal (interp-flags->make-ites new-x) (bool-fix make-ites))))
Theorem:
(defthm !interp-flags->make-ites-equiv-under-mask (b* ((?new-x (!interp-flags->make-ites make-ites x))) (interp-flags-equiv-under-mask new-x x -17)))