		Search-engine friendly clone of the ACL2 documentation.

Npn4

Npn4->truth-idx

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

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

Definitions and Theorems

Function: npn4->truth-idx

(defun npn4->truth-idx (x)
  (declare (xargs :guard (npn4-p x)))
  (mbe :logic
       (let ((x (npn4-fix x)))
         (part-select x :low 0 :width 16))
       :exec (the (unsigned-byte 16)
                  (logand (the (unsigned-byte 16) 65535)
                          (the (unsigned-byte 27) x)))))

Theorem: truth-idx-p-of-npn4->truth-idx

(defthm truth-idx-p-of-npn4->truth-idx
  (b* ((truth-idx (npn4->truth-idx x)))
    (truth-idx-p truth-idx))
  :rule-classes :rewrite)

Theorem: npn4->truth-idx-of-npn4-fix-x

(defthm npn4->truth-idx-of-npn4-fix-x
  (equal (npn4->truth-idx (npn4-fix x))
         (npn4->truth-idx x)))

Theorem: npn4->truth-idx-npn4-equiv-congruence-on-x

(defthm npn4->truth-idx-npn4-equiv-congruence-on-x
  (implies (npn4-equiv x x-equiv)
           (equal (npn4->truth-idx x)
                  (npn4->truth-idx x-equiv)))
  :rule-classes :congruence)

Theorem: npn4->truth-idx-of-npn4

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

Theorem: npn4->truth-idx-of-write-with-mask

(defthm npn4->truth-idx-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) 65535)
              0))
  (equal (npn4->truth-idx x)
         (npn4->truth-idx acl2::y))))