Update the |AIGNET|::|CHOICE| field of a simpcode bit structure.
(!simpcode->choice choice x) → new-x
Function:
(defun !simpcode->choice (choice x) (declare (xargs :guard (and (bitp choice) (simpcode-p x)))) (mbe :logic (b* ((choice (mbe :logic (bfix choice) :exec choice)) (x (simpcode-fix x))) (part-install choice x :width 1 :low 3)) :exec (the (unsigned-byte 4) (logior (the (unsigned-byte 4) (logand (the (unsigned-byte 4) x) (the (signed-byte 5) -9))) (the (unsigned-byte 4) (ash (the (unsigned-byte 1) choice) 3))))))
Theorem:
(defthm simpcode-p-of-!simpcode->choice (b* ((new-x (!simpcode->choice choice x))) (simpcode-p new-x)) :rule-classes :rewrite)
Theorem:
(defthm !simpcode->choice-of-bfix-choice (equal (!simpcode->choice (bfix choice) x) (!simpcode->choice choice x)))
Theorem:
(defthm !simpcode->choice-bit-equiv-congruence-on-choice (implies (bit-equiv choice choice-equiv) (equal (!simpcode->choice choice x) (!simpcode->choice choice-equiv x))) :rule-classes :congruence)
Theorem:
(defthm !simpcode->choice-of-simpcode-fix-x (equal (!simpcode->choice choice (simpcode-fix x)) (!simpcode->choice choice x)))
Theorem:
(defthm !simpcode->choice-simpcode-equiv-congruence-on-x (implies (simpcode-equiv x x-equiv) (equal (!simpcode->choice choice x) (!simpcode->choice choice x-equiv))) :rule-classes :congruence)
Theorem:
(defthm !simpcode->choice-is-simpcode (equal (!simpcode->choice choice x) (change-simpcode x :choice choice)))
Theorem:
(defthm simpcode->choice-of-!simpcode->choice (b* ((?new-x (!simpcode->choice choice x))) (equal (simpcode->choice new-x) (bfix choice))))
Theorem:
(defthm !simpcode->choice-equiv-under-mask (b* ((?new-x (!simpcode->choice choice x))) (simpcode-equiv-under-mask new-x x 7)))