		Search-engine friendly clone of the ACL2 documentation.

Npn4

Npn4->perm

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

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

Definitions and Theorems

Function: npn4->perm

(defun npn4->perm (x)
  (declare (xargs :guard (npn4-p x)))
  (mbe :logic
       (let ((x (npn4-fix x)))
         (part-select x :low 21 :width 6))
       :exec (the (unsigned-byte 6)
                  (logand (the (unsigned-byte 6) 63)
                          (the (unsigned-byte 6)
                               (ash (the (unsigned-byte 27) x)
                                    -21))))))

Theorem: perm4p-of-npn4->perm

(defthm perm4p-of-npn4->perm
  (b* ((perm (npn4->perm x)))
    (perm4p perm))
  :rule-classes :rewrite)

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

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

Theorem: npn4->perm-of-npn4

(defthm npn4->perm-of-npn4
  (equal (npn4->perm (npn4 truth-idx negate polarity perm))
         (perm4-fix perm)))

Theorem: npn4->perm-of-write-with-mask

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