• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
      • Aig
      • Satlink
      • Truth
      • Ubdds
      • Bdd
      • Faig
      • Bed
        • Bed-op-p
          • Bed-op-eval
          • Bed-op-fix
            • Bed-op-xor
            • Bed-op-true
            • Bed-op-orc2
            • Bed-op-orc1
            • Bed-op-not2
            • Bed-op-not1
            • Bed-op-nor
            • Bed-op-nand
            • Bed-op-ior
            • Bed-op-false
            • Bed-op-eqv
            • Bed-op-arg2
            • Bed-op-arg1
            • Bed-op-andc2
            • Bed-op-andc1
            • Bed-op-and
            • Bed-op-fix$
          • Bed-from-aig
          • Bed-mk1
          • Bed-eval
          • Up
          • Aig-translation
        • 4v
      • Debugging
      • Projects
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Bed-op-p

    Bed-op-fix

    Fixing function for bed-op-ps.

    Signature
    (bed-op-fix x) → op
    Returns
    op — Type (bed-op-p op).

    Definitions and Theorems

    Function: bed-op-fix$inline

    (defun bed-op-fix$inline (x)
           (declare (xargs :guard t))
           (let ((__function__ 'bed-op-fix))
                (declare (ignorable __function__))
                (the (unsigned-byte 4)
                     (logand 15 (the integer (ifix x))))))

    Theorem: bed-op-p-of-bed-op-fix

    (defthm bed-op-p-of-bed-op-fix
            (b* ((op (bed-op-fix$inline x)))
                (bed-op-p op))
            :rule-classes :rewrite)

    Theorem: bed-op-fix-when-bed-op-p

    (defthm bed-op-fix-when-bed-op-p
            (implies (bed-op-p x)
                     (equal (bed-op-fix x) x)))