		Search-engine friendly clone of the ACL2 documentation.

Npn4

!npn4->perm

Update the |TRUTH|::|PERM| field of a npn4 bit structure.

Signature
(!npn4->perm perm x) → new-x
Arguments: perm — Guard (perm4p perm).; x — Guard (npn4-p x).
Returns: new-x — Type (npn4-p new-x).

Definitions and Theorems

Function: !npn4->perm

(defun !npn4->perm (perm x)
  (declare (xargs :guard (and (perm4p perm) (npn4-p x))))
  (mbe :logic
       (b* ((perm (mbe :logic (perm4-fix perm)
                       :exec perm))
            (x (npn4-fix x)))
         (part-install perm x :width 6 :low 21))
       :exec
       (the (unsigned-byte 27)
            (logior (the (unsigned-byte 27)
                         (logand (the (unsigned-byte 27) x)
                                 (the (signed-byte 28) -132120577)))
                    (the (unsigned-byte 27)
                         (ash (the (unsigned-byte 6) perm)
                              21))))))

Theorem: npn4-p-of-!npn4->perm

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

Theorem: !npn4->perm-of-perm4-fix-perm

(defthm !npn4->perm-of-perm4-fix-perm
  (equal (!npn4->perm (perm4-fix perm) x)
         (!npn4->perm perm x)))

Theorem: !npn4->perm-perm4-equiv-congruence-on-perm

(defthm !npn4->perm-perm4-equiv-congruence-on-perm
  (implies (perm4-equiv perm perm-equiv)
           (equal (!npn4->perm perm x)
                  (!npn4->perm perm-equiv x)))
  :rule-classes :congruence)

Theorem: !npn4->perm-of-npn4-fix-x

(defthm !npn4->perm-of-npn4-fix-x
  (equal (!npn4->perm perm (npn4-fix x))
         (!npn4->perm perm x)))

Theorem: !npn4->perm-npn4-equiv-congruence-on-x

(defthm !npn4->perm-npn4-equiv-congruence-on-x
  (implies (npn4-equiv x x-equiv)
           (equal (!npn4->perm perm x)
                  (!npn4->perm perm x-equiv)))
  :rule-classes :congruence)

Theorem: !npn4->perm-is-npn4

(defthm !npn4->perm-is-npn4
  (equal (!npn4->perm perm x)
         (change-npn4 x :perm perm)))

Theorem: npn4->perm-of-!npn4->perm

(defthm npn4->perm-of-!npn4->perm
  (b* ((?new-x (!npn4->perm perm x)))
    (equal (npn4->perm new-x)
           (perm4-fix perm))))

Theorem: !npn4->perm-equiv-under-mask

(defthm !npn4->perm-equiv-under-mask
  (b* ((?new-x (!npn4->perm perm x)))
    (npn4-equiv-under-mask new-x x 2097151)))