• 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-<=
        • 4v-alist-<=
        • 4v-list-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Debugging
  • Projects
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 4v

4v-<=

Four-valued lattice-ordering comparison.

(4v-<= a b) is true when A is B or X.

This is a partial ordering on the four-valued constants. We generally just write a <= b instead of (4v-<= a b).

We say that X is smaller than any other value. Furthermore, this is reflexive, i.e., A <= A for any value A. Finally, there is no order imposed between T, F, and Z.

Drawn as a lattice, the picture is:

T     F     Z
 \    |    /
   \  |  /
     \|/
      X

This ordering plays a key role in 4v-monotonicity.

Definitions and Theorems

Function: 4v-<=$inline

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

Theorem: 4v-<=-x

(defthm 4v-<=-x (4v-<= (4vx) x))

Theorem: 4v-<=-refl

(defthm 4v-<=-refl (4v-<= a a))

Theorem: 4v-<=-trans1

(defthm 4v-<=-trans1
        (implies (and (4v-<= a b) (4v-<= b c))
                 (4v-<= a c)))

Theorem: 4v-<=-trans2

(defthm 4v-<=-trans2
        (implies (and (4v-<= b c) (4v-<= a b))
                 (4v-<= a c)))

Theorem: 4v-<=-of-4v-fix-1

(defthm 4v-<=-of-4v-fix-1
        (equal (4v-<= (4v-fix a) b)
               (4v-<= a b)))

Theorem: 4v-<=-of-4v-fix-2

(defthm 4v-<=-of-4v-fix-2
        (equal (4v-<= a (4v-fix b))
               (4v-<= a b)))

Theorem: 4v-equiv-implies-equal-4v-<=-2

(defthm 4v-equiv-implies-equal-4v-<=-2
        (implies (4v-equiv b b-equiv)
                 (equal (4v-<= a b) (4v-<= a b-equiv)))
        :rule-classes (:congruence))

Theorem: 4v-equiv-implies-equal-4v-<=-1

(defthm 4v-equiv-implies-equal-4v-<=-1
        (implies (4v-equiv a a-equiv)
                 (equal (4v-<= a b) (4v-<= a-equiv b)))
        :rule-classes (:congruence))

Subtopics

4v-alist-<=

Extension of 4v-<= to four-valued alists.

4v-list-<=

Extension of 4v-<= to four-valued lists.