		Search-engine friendly clone of the ACL2 documentation.

Undocumented

Simpcode

An 4-bit unsigned bitstruct type.

This is a bitstruct type introduced by fty::defbitstruct, represented as a unsigned 4-bit integer.

Fields

neg — bit
xor — bit
identity — bit
choice — bit

Definitions and Theorems

Function: simpcode-p

(defun simpcode-p (x)
  (declare (xargs :guard t))
  (let ((__function__ 'simpcode-p))
    (declare (ignorable __function__))
    (mbe :logic (unsigned-byte-p 4 x)
         :exec (and (natp x) (< x 16)))))

Theorem: simpcode-p-when-unsigned-byte-p

(defthm simpcode-p-when-unsigned-byte-p
  (implies (unsigned-byte-p 4 x)
           (simpcode-p x)))

Theorem: unsigned-byte-p-when-simpcode-p

(defthm unsigned-byte-p-when-simpcode-p
  (implies (simpcode-p x)
           (unsigned-byte-p 4 x)))

Theorem: simpcode-p-compound-recognizer

(defthm simpcode-p-compound-recognizer
  (implies (simpcode-p x) (natp x))
  :rule-classes :compound-recognizer)

Function: simpcode-fix

(defun simpcode-fix (x)
  (declare (xargs :guard (simpcode-p x)))
  (let ((__function__ 'simpcode-fix))
    (declare (ignorable __function__))
    (mbe :logic (loghead 4 x) :exec x)))

Theorem: simpcode-p-of-simpcode-fix

(defthm simpcode-p-of-simpcode-fix
  (b* ((fty::fixed (simpcode-fix x)))
    (simpcode-p fty::fixed))
  :rule-classes :rewrite)

Theorem: simpcode-fix-when-simpcode-p

(defthm simpcode-fix-when-simpcode-p
  (implies (simpcode-p x)
           (equal (simpcode-fix x) x)))

Function: simpcode-equiv$inline

(defun simpcode-equiv$inline (x acl2::y)
  (declare (xargs :guard (and (simpcode-p x)
                              (simpcode-p acl2::y))))
  (equal (simpcode-fix x)
         (simpcode-fix acl2::y)))

Theorem: simpcode-equiv-is-an-equivalence

(defthm simpcode-equiv-is-an-equivalence
  (and (booleanp (simpcode-equiv x y))
       (simpcode-equiv x x)
       (implies (simpcode-equiv x y)
                (simpcode-equiv y x))
       (implies (and (simpcode-equiv x y)
                     (simpcode-equiv y z))
                (simpcode-equiv x z)))
  :rule-classes (:equivalence))

Theorem: simpcode-equiv-implies-equal-simpcode-fix-1

(defthm simpcode-equiv-implies-equal-simpcode-fix-1
  (implies (simpcode-equiv x x-equiv)
           (equal (simpcode-fix x)
                  (simpcode-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: simpcode-fix-under-simpcode-equiv

(defthm simpcode-fix-under-simpcode-equiv
  (simpcode-equiv (simpcode-fix x) x)
  :rule-classes (:rewrite :rewrite-quoted-constant))

Theorem: simpcode-fix-of-simpcode-fix-x

(defthm simpcode-fix-of-simpcode-fix-x
  (equal (simpcode-fix (simpcode-fix x))
         (simpcode-fix x)))

Theorem: simpcode-fix-simpcode-equiv-congruence-on-x

(defthm simpcode-fix-simpcode-equiv-congruence-on-x
  (implies (simpcode-equiv x x-equiv)
           (equal (simpcode-fix x)
                  (simpcode-fix x-equiv)))
  :rule-classes :congruence)

Function: simpcode

(defun simpcode (neg xor identity choice)
  (declare (xargs :guard (and (bitp neg)
                              (bitp xor)
                              (bitp identity)
                              (bitp choice))))
  (let ((__function__ 'simpcode))
    (declare (ignorable __function__))
    (b* ((neg (mbe :logic (bfix neg) :exec neg))
         (xor (mbe :logic (bfix xor) :exec xor))
         (identity (mbe :logic (bfix identity)
                        :exec identity))
         (choice (mbe :logic (bfix choice)
                      :exec choice)))
      (logapp 1 neg
              (logapp 1 xor (logapp 1 identity choice))))))

Theorem: simpcode-p-of-simpcode

(defthm simpcode-p-of-simpcode
  (b* ((simpcode (simpcode neg xor identity choice)))
    (simpcode-p simpcode))
  :rule-classes :rewrite)

Theorem: simpcode-of-bfix-neg

(defthm simpcode-of-bfix-neg
  (equal (simpcode (bfix neg)
                   xor identity choice)
         (simpcode neg xor identity choice)))

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

(defthm simpcode-bit-equiv-congruence-on-neg
  (implies (bit-equiv neg neg-equiv)
           (equal (simpcode neg xor identity choice)
                  (simpcode neg-equiv xor identity choice)))
  :rule-classes :congruence)

Theorem: simpcode-of-bfix-xor

(defthm simpcode-of-bfix-xor
  (equal (simpcode neg (bfix xor)
                   identity choice)
         (simpcode neg xor identity choice)))

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

(defthm simpcode-bit-equiv-congruence-on-xor
  (implies (bit-equiv xor xor-equiv)
           (equal (simpcode neg xor identity choice)
                  (simpcode neg xor-equiv identity choice)))
  :rule-classes :congruence)

Theorem: simpcode-of-bfix-identity

(defthm simpcode-of-bfix-identity
  (equal (simpcode neg xor (bfix identity)
                   choice)
         (simpcode neg xor identity choice)))

Theorem: simpcode-bit-equiv-congruence-on-identity

(defthm simpcode-bit-equiv-congruence-on-identity
  (implies (bit-equiv identity identity-equiv)
           (equal (simpcode neg xor identity choice)
                  (simpcode neg xor identity-equiv choice)))
  :rule-classes :congruence)

Theorem: simpcode-of-bfix-choice

(defthm simpcode-of-bfix-choice
  (equal (simpcode neg xor identity (bfix choice))
         (simpcode neg xor identity choice)))

Theorem: simpcode-bit-equiv-congruence-on-choice

(defthm simpcode-bit-equiv-congruence-on-choice
  (implies (bit-equiv choice choice-equiv)
           (equal (simpcode neg xor identity choice)
                  (simpcode neg xor identity choice-equiv)))
  :rule-classes :congruence)

Function: simpcode-equiv-under-mask

(defun simpcode-equiv-under-mask (x x1 mask)
  (declare (xargs :guard (and (simpcode-p x)
                              (simpcode-p x1)
                              (integerp mask))))
  (let ((__function__ 'simpcode-equiv-under-mask))
    (declare (ignorable __function__))
    (fty::int-equiv-under-mask (simpcode-fix x)
                               (simpcode-fix x1)
                               mask)))

Theorem: simpcode-equiv-under-mask-of-simpcode-fix-x

(defthm simpcode-equiv-under-mask-of-simpcode-fix-x
  (equal (simpcode-equiv-under-mask (simpcode-fix x)
                                    x1 mask)
         (simpcode-equiv-under-mask x x1 mask)))

Theorem: simpcode-equiv-under-mask-simpcode-equiv-congruence-on-x

(defthm simpcode-equiv-under-mask-simpcode-equiv-congruence-on-x
  (implies (simpcode-equiv x x-equiv)
           (equal (simpcode-equiv-under-mask x x1 mask)
                  (simpcode-equiv-under-mask x-equiv x1 mask)))
  :rule-classes :congruence)

Theorem: simpcode-equiv-under-mask-of-simpcode-fix-x1

(defthm simpcode-equiv-under-mask-of-simpcode-fix-x1
  (equal (simpcode-equiv-under-mask x (simpcode-fix x1)
                                    mask)
         (simpcode-equiv-under-mask x x1 mask)))

Theorem: simpcode-equiv-under-mask-simpcode-equiv-congruence-on-x1

(defthm simpcode-equiv-under-mask-simpcode-equiv-congruence-on-x1
  (implies (simpcode-equiv x1 x1-equiv)
           (equal (simpcode-equiv-under-mask x x1 mask)
                  (simpcode-equiv-under-mask x x1-equiv mask)))
  :rule-classes :congruence)

Theorem: simpcode-equiv-under-mask-of-ifix-mask

(defthm simpcode-equiv-under-mask-of-ifix-mask
  (equal (simpcode-equiv-under-mask x x1 (ifix mask))
         (simpcode-equiv-under-mask x x1 mask)))

Theorem: simpcode-equiv-under-mask-int-equiv-congruence-on-mask

(defthm simpcode-equiv-under-mask-int-equiv-congruence-on-mask
  (implies (int-equiv mask mask-equiv)
           (equal (simpcode-equiv-under-mask x x1 mask)
                  (simpcode-equiv-under-mask x x1 mask-equiv)))
  :rule-classes :congruence)

Function: simpcode->neg

(defun simpcode->neg (x)
  (declare (xargs :guard (simpcode-p x)))
  (mbe :logic
       (let ((x (simpcode-fix x)))
         (part-select x :low 0 :width 1))
       :exec (the (unsigned-byte 1)
                  (logand (the (unsigned-byte 1) 1)
                          (the (unsigned-byte 4) x)))))

Theorem: bitp-of-simpcode->neg

(defthm bitp-of-simpcode->neg
  (b* ((neg (simpcode->neg x)))
    (bitp neg))
  :rule-classes :rewrite)

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

(defthm simpcode->neg-of-simpcode-fix-x
  (equal (simpcode->neg (simpcode-fix x))
         (simpcode->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 x)
                  (simpcode->neg x-equiv)))
  :rule-classes :congruence)

Theorem: simpcode->neg-of-simpcode

(defthm simpcode->neg-of-simpcode
  (equal (simpcode->neg (simpcode neg xor identity choice))
         (bfix neg)))

Theorem: simpcode->neg-of-write-with-mask

(defthm simpcode->neg-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x simpcode-equiv-under-mask)
   (simpcode-equiv-under-mask x acl2::y fty::mask)
   (equal (logand (lognot fty::mask) 1) 0))
  (equal (simpcode->neg x)
         (simpcode->neg acl2::y))))

Function: simpcode->xor

(defun simpcode->xor (x)
 (declare (xargs :guard (simpcode-p x)))
 (mbe
     :logic
     (let ((x (simpcode-fix x)))
       (part-select x :low 1 :width 1))
     :exec (the (unsigned-byte 1)
                (logand (the (unsigned-byte 1) 1)
                        (the (unsigned-byte 3)
                             (ash (the (unsigned-byte 4) x) -1))))))

Theorem: bitp-of-simpcode->xor

(defthm bitp-of-simpcode->xor
  (b* ((xor (simpcode->xor x)))
    (bitp xor))
  :rule-classes :rewrite)

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

(defthm simpcode->xor-of-simpcode-fix-x
  (equal (simpcode->xor (simpcode-fix x))
         (simpcode->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 x)
                  (simpcode->xor x-equiv)))
  :rule-classes :congruence)

Theorem: simpcode->xor-of-simpcode

(defthm simpcode->xor-of-simpcode
  (equal (simpcode->xor (simpcode neg xor identity choice))
         (bfix xor)))

Theorem: simpcode->xor-of-write-with-mask

(defthm simpcode->xor-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x simpcode-equiv-under-mask)
   (simpcode-equiv-under-mask x acl2::y fty::mask)
   (equal (logand (lognot fty::mask) 2) 0))
  (equal (simpcode->xor x)
         (simpcode->xor acl2::y))))

Function: simpcode->identity

(defun simpcode->identity (x)
 (declare (xargs :guard (simpcode-p x)))
 (mbe
     :logic
     (let ((x (simpcode-fix x)))
       (part-select x :low 2 :width 1))
     :exec (the (unsigned-byte 1)
                (logand (the (unsigned-byte 1) 1)
                        (the (unsigned-byte 2)
                             (ash (the (unsigned-byte 4) x) -2))))))

Theorem: bitp-of-simpcode->identity

(defthm bitp-of-simpcode->identity
  (b* ((identity (simpcode->identity x)))
    (bitp identity))
  :rule-classes :rewrite)

Theorem: simpcode->identity-of-simpcode-fix-x

(defthm simpcode->identity-of-simpcode-fix-x
  (equal (simpcode->identity (simpcode-fix x))
         (simpcode->identity x)))

Theorem: simpcode->identity-simpcode-equiv-congruence-on-x

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

Theorem: simpcode->identity-of-simpcode

(defthm simpcode->identity-of-simpcode
  (equal (simpcode->identity (simpcode neg xor identity choice))
         (bfix identity)))

Theorem: simpcode->identity-of-write-with-mask

(defthm simpcode->identity-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x simpcode-equiv-under-mask)
   (simpcode-equiv-under-mask x acl2::y fty::mask)
   (equal (logand (lognot fty::mask) 4) 0))
  (equal (simpcode->identity x)
         (simpcode->identity acl2::y))))

Function: simpcode->choice

(defun simpcode->choice (x)
 (declare (xargs :guard (simpcode-p x)))
 (mbe
     :logic
     (let ((x (simpcode-fix x)))
       (part-select x :low 3 :width 1))
     :exec (the (unsigned-byte 1)
                (logand (the (unsigned-byte 1) 1)
                        (the (unsigned-byte 1)
                             (ash (the (unsigned-byte 4) x) -3))))))

Theorem: bitp-of-simpcode->choice

(defthm bitp-of-simpcode->choice
  (b* ((choice (simpcode->choice x)))
    (bitp choice))
  :rule-classes :rewrite)

Theorem: simpcode->choice-of-simpcode-fix-x

(defthm simpcode->choice-of-simpcode-fix-x
  (equal (simpcode->choice (simpcode-fix x))
         (simpcode->choice x)))

Theorem: simpcode->choice-simpcode-equiv-congruence-on-x

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

Theorem: simpcode->choice-of-simpcode

(defthm simpcode->choice-of-simpcode
  (equal (simpcode->choice (simpcode neg xor identity choice))
         (bfix choice)))

Theorem: simpcode->choice-of-write-with-mask

(defthm simpcode->choice-of-write-with-mask
 (implies
  (and
   (fty::bitstruct-read-over-write-hyps x simpcode-equiv-under-mask)
   (simpcode-equiv-under-mask x acl2::y fty::mask)
   (equal (logand (lognot fty::mask) 8) 0))
  (equal (simpcode->choice x)
         (simpcode->choice acl2::y))))

Theorem: simpcode-fix-in-terms-of-simpcode

(defthm simpcode-fix-in-terms-of-simpcode
  (equal (simpcode-fix x)
         (change-simpcode x)))

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)))

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)))

Function: !simpcode->identity

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

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

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

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

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

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

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

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

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

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

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

Theorem: !simpcode->identity-is-simpcode

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

Theorem: simpcode->identity-of-!simpcode->identity

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

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

(defthm !simpcode->identity-equiv-under-mask
  (b* ((?new-x (!simpcode->identity identity x)))
    (simpcode-equiv-under-mask new-x x -5)))

Function: !simpcode->choice

(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: simpcode-p-of-!simpcode->choice

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

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

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

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

(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: !simpcode->choice-of-simpcode-fix-x

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

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

(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: !simpcode->choice-is-simpcode

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

Theorem: simpcode->choice-of-!simpcode->choice

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

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

(defthm !simpcode->choice-equiv-under-mask
  (b* ((?new-x (!simpcode->choice choice x)))
    (simpcode-equiv-under-mask new-x x 7)))

Function: simpcode-debug

(defun simpcode-debug (x)
  (declare (xargs :guard (simpcode-p x)))
  (let ((__function__ 'simpcode-debug))
    (declare (ignorable __function__))
    (b* (((simpcode x)))
      (cons (cons 'neg x.neg)
            (cons (cons 'xor x.xor)
                  (cons (cons 'identity x.identity)
                        (cons (cons 'choice x.choice) nil)))))))

Theorem: simpcode-debug-of-simpcode-fix-x

(defthm simpcode-debug-of-simpcode-fix-x
  (equal (simpcode-debug (simpcode-fix x))
         (simpcode-debug x)))

Theorem: simpcode-debug-simpcode-equiv-congruence-on-x

(defthm simpcode-debug-simpcode-equiv-congruence-on-x
  (implies (simpcode-equiv x x-equiv)
           (equal (simpcode-debug x)
                  (simpcode-debug x-equiv)))
  :rule-classes :congruence)

Subtopics

!simpcode->identity: Update the |COMMON-LISP|::|IDENTITY| field of a simpcode bit structure.
!simpcode->choice: Update the |AIGNET|::|CHOICE| field of a simpcode bit structure.
!simpcode->xor: Update the |ACL2|::|XOR| field of a simpcode bit structure.
!simpcode->neg: Update the |AIGNET|::|NEG| field of a simpcode bit structure.
Simpcode-fix: Fixing function for simpcode bit structures.
Simpcode-p: Recognizer for simpcode bit structures.
Simpcode->identity: Access the |COMMON-LISP|::|IDENTITY| field of a simpcode bit structure.
Simpcode->choice: Access the |AIGNET|::|CHOICE| field of a simpcode bit structure.
Simpcode->xor: Access the |ACL2|::|XOR| field of a simpcode bit structure.
Simpcode->neg: Access the |AIGNET|::|NEG| field of a simpcode bit structure.