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