• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
      • Arithmetic
      • Bit-vectors
        • Sparseint
        • Bitops
        • Bv
        • Ihs
          • Logops-definitions
            • Logops-byte-functions
            • Defword
            • Defbytetype
            • Logext
            • Logrev
            • Loghead
            • Logops-bit-functions
              • Simplify-bit-functions
              • B-eqv
              • B-xor
              • B-orc2
              • B-orc1
              • B-nor
              • B-nand
              • B-ite
              • B-ior
              • B-andc2
              • B-andc1
              • B-and
                • B-not
              • Logtail
              • Logapp
              • Logsat
              • Binary--
              • Logcdr
              • Logcar
              • Logcons
              • Logbit
              • Logextu
              • Lshu
              • Logrpl
              • Ashu
              • Logmaskp
              • Lognotu
              • Logmask
              • Ifloor
              • Imod
              • Bitmaskp
              • Bfix
              • Logite
              • Expt2
              • *logops-functions*
              • Zbp
              • Word/bit-macros
              • Logops-definitions-theory
              • Logops-functions
              • Lbfix
              • Logextu-guard
              • Lshu-guard
              • Logtail-guard
              • Logrpl-guard
              • Logrev-guard
              • Lognotu-guard
              • Logmask-guard
              • Loghead-guard
              • Logext-guard
              • Logbit-guard
              • Logapp-guard
              • Ashu-guard
            • Math-lemmas
            • Ihs-theories
            • Ihs-init
            • Logops
          • Rtl
        • Algebra
    • Logops-bit-functions

    B-and

    Conjunction for bitps.

    Signature
    (b-and i j) → bit
    Arguments
    i — Guard (bitp i).
    j — Guard (bitp j).
    Returns
    bit — Type (bitp bit).

    Definitions and Theorems

    Function: b-and$inline

    (defun b-and$inline (i j)
           (declare (xargs :guard (and (bitp i) (bitp j))))
           (let ((__function__ 'b-and))
                (declare (ignorable __function__))
                (mbe :logic (if (zbp i) 0 (if (zbp j) 0 1))
                     :exec (the (unsigned-byte 1)
                                (logand (the (unsigned-byte 1) i)
                                        (the (unsigned-byte 1) j))))))

    Theorem: bitp-of-b-and

    (defthm bitp-of-b-and
            (b* ((bit (b-and$inline i j)))
                (bitp bit))
            :rule-classes :type-prescription)