		Search-engine friendly clone of the ACL2 documentation.

Simpcode

!simpcode->neg

Update the |AIGNET|::|NEG| field of a simpcode bit structure.

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

Definitions and Theorems

Function: !simpcode->neg

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

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

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

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

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

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

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

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

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

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

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

Theorem: !simpcode->neg-is-simpcode

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

Theorem: simpcode->neg-of-!simpcode->neg

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

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

(defthm !simpcode->neg-equiv-under-mask
  (b* ((?new-x (!simpcode->neg neg x)))
    (simpcode-equiv-under-mask new-x x -2)))