		Search-engine friendly clone of the ACL2 documentation.

Interp-flags

!interp-flags->if-merge-last-chance

Update the |FGL|::|IF-MERGE-LAST-CHANCE| field of a interp-flags bit structure.

Signature
(!interp-flags->if-merge-last-chance if-merge-last-chance x) → new-x
Arguments: if-merge-last-chance — Guard (booleanp if-merge-last-chance).; x — Guard (interp-flags-p x).
Returns: new-x — Type (interp-flags-p new-x).

Definitions and Theorems

Function: !interp-flags->if-merge-last-chance

(defun !interp-flags->if-merge-last-chance (if-merge-last-chance x)
  (declare (xargs :guard (and (booleanp if-merge-last-chance)
                              (interp-flags-p x))))
  (mbe :logic
       (b* ((if-merge-last-chance (bool->bit if-merge-last-chance))
            (x (interp-flags-fix x)))
         (acl2::part-install if-merge-last-chance 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 if-merge-last-chance))
                              5))))))

Theorem: interp-flags-p-of-!interp-flags->if-merge-last-chance

(defthm interp-flags-p-of-!interp-flags->if-merge-last-chance
 (b*
  ((new-x
      (!interp-flags->if-merge-last-chance if-merge-last-chance x)))
  (interp-flags-p new-x))
 :rule-classes :rewrite)

Theorem: !interp-flags->if-merge-last-chance-of-bool-fix-if-merge-last-chance

(defthm
 !interp-flags->if-merge-last-chance-of-bool-fix-if-merge-last-chance
 (equal
      (!interp-flags->if-merge-last-chance
           (bool-fix if-merge-last-chance)
           x)
      (!interp-flags->if-merge-last-chance if-merge-last-chance x)))

Theorem: !interp-flags->if-merge-last-chance-iff-congruence-on-if-merge-last-chance

(defthm
 !interp-flags->if-merge-last-chance-iff-congruence-on-if-merge-last-chance
 (implies
   (iff if-merge-last-chance
        if-merge-last-chance-equiv)
   (equal
        (!interp-flags->if-merge-last-chance if-merge-last-chance x)
        (!interp-flags->if-merge-last-chance
             if-merge-last-chance-equiv x)))
 :rule-classes :congruence)

Theorem: !interp-flags->if-merge-last-chance-of-interp-flags-fix-x

(defthm !interp-flags->if-merge-last-chance-of-interp-flags-fix-x
 (equal
      (!interp-flags->if-merge-last-chance if-merge-last-chance
                                           (interp-flags-fix x))
      (!interp-flags->if-merge-last-chance if-merge-last-chance x)))

Theorem: !interp-flags->if-merge-last-chance-interp-flags-equiv-congruence-on-x

(defthm
 !interp-flags->if-merge-last-chance-interp-flags-equiv-congruence-on-x
 (implies
   (interp-flags-equiv x x-equiv)
   (equal
        (!interp-flags->if-merge-last-chance if-merge-last-chance x)
        (!interp-flags->if-merge-last-chance
             if-merge-last-chance x-equiv)))
 :rule-classes :congruence)

Theorem: !interp-flags->if-merge-last-chance-is-interp-flags

(defthm !interp-flags->if-merge-last-chance-is-interp-flags
 (equal
  (!interp-flags->if-merge-last-chance if-merge-last-chance x)
  (change-interp-flags x
                       :if-merge-last-chance if-merge-last-chance)))

Theorem: interp-flags->if-merge-last-chance-of-!interp-flags->if-merge-last-chance

(defthm
 interp-flags->if-merge-last-chance-of-!interp-flags->if-merge-last-chance
 (b*
  ((?new-x
      (!interp-flags->if-merge-last-chance if-merge-last-chance x)))
  (equal (interp-flags->if-merge-last-chance new-x)
         (bool-fix if-merge-last-chance))))

Theorem: !interp-flags->if-merge-last-chance-equiv-under-mask

(defthm !interp-flags->if-merge-last-chance-equiv-under-mask
 (b*
  ((?new-x
      (!interp-flags->if-merge-last-chance if-merge-last-chance x)))
  (interp-flags-equiv-under-mask new-x x 31)))