		Search-engine friendly clone of the ACL2 documentation.

Simpcode

!simpcode->xor

Update the |ACL2|::|XOR| field of a simpcode bit structure.

Signature
(!simpcode->xor xor x) → new-x
Arguments: xor — Guard (bitp xor).; x — Guard (simpcode-p x).
Returns: new-x — Type (simpcode-p new-x).

Definitions and Theorems

Function: !simpcode->xor

(defun !simpcode->xor (xor x)
 (declare (xargs :guard (and (bitp xor) (simpcode-p x))))
 (mbe
    :logic
    (b* ((xor (mbe :logic (bfix xor) :exec xor))
         (x (simpcode-fix x)))
      (part-install xor x :width 1 :low 1))
    :exec (the (unsigned-byte 4)
               (logior (the (unsigned-byte 4)
                            (logand (the (unsigned-byte 4) x)
                                    (the (signed-byte 3) -3)))
                       (the (unsigned-byte 2)
                            (ash (the (unsigned-byte 1) xor) 1))))))

Theorem: simpcode-p-of-!simpcode->xor

(defthm simpcode-p-of-!simpcode->xor
  (b* ((new-x (!simpcode->xor xor x)))
    (simpcode-p new-x))
  :rule-classes :rewrite)

Theorem: !simpcode->xor-of-bfix-xor

(defthm !simpcode->xor-of-bfix-xor
  (equal (!simpcode->xor (bfix xor) x)
         (!simpcode->xor xor x)))

Theorem: !simpcode->xor-bit-equiv-congruence-on-xor

(defthm !simpcode->xor-bit-equiv-congruence-on-xor
  (implies (bit-equiv xor xor-equiv)
           (equal (!simpcode->xor xor x)
                  (!simpcode->xor xor-equiv x)))
  :rule-classes :congruence)

Theorem: !simpcode->xor-of-simpcode-fix-x

(defthm !simpcode->xor-of-simpcode-fix-x
  (equal (!simpcode->xor xor (simpcode-fix x))
         (!simpcode->xor xor x)))

Theorem: !simpcode->xor-simpcode-equiv-congruence-on-x

(defthm !simpcode->xor-simpcode-equiv-congruence-on-x
  (implies (simpcode-equiv x x-equiv)
           (equal (!simpcode->xor xor x)
                  (!simpcode->xor xor x-equiv)))
  :rule-classes :congruence)

Theorem: !simpcode->xor-is-simpcode

(defthm !simpcode->xor-is-simpcode
  (equal (!simpcode->xor xor x)
         (change-simpcode x :xor xor)))

Theorem: simpcode->xor-of-!simpcode->xor

(defthm simpcode->xor-of-!simpcode->xor
  (b* ((?new-x (!simpcode->xor xor x)))
    (equal (simpcode->xor new-x)
           (bfix xor))))

Theorem: !simpcode->xor-equiv-under-mask

(defthm !simpcode->xor-equiv-under-mask
  (b* ((?new-x (!simpcode->xor xor x)))
    (simpcode-equiv-under-mask new-x x -3)))