• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 4v

4v-fix

Fixing function for four-valued constants.

(4v-fix a) interprets a as a four-valued constant. Any non-4vp objects are coerced to X.

Definitions and Theorems

Function: 4v-fix$inline

(defun 4v-fix$inline (a)
       (declare (xargs :guard t))
       (mbe :logic (if (4vp a) a (4vx))
            :exec (if (or (eq a (4vt))
                          (eq a (4vf))
                          (eq a (4vz)))
                      a (4vx))))

Theorem: 4v-fix-when-4vp

(defthm 4v-fix-when-4vp
        (implies (4vp x) (equal (4v-fix x) x)))

Theorem: 4vp-of-4v-fix

(defthm 4vp-of-4v-fix (4vp (4v-fix x)))