# 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.