		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.