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