The monotonicity property satisfied by all 4v-operations.

All of our primitive four-valued operations satisfy the following monotonicity property, where <= denotes 4v-<=:

Whenever a <= b, f(a) <= f(b).

A higher-arity function is monotonic if it is monotonic with respect to each of its arguments, e.g., a binary function is monotonic if:

Whenever a1 <= a2, f(a1, b1) <= f(a2, b2), and

Whenever b1 <= b2, f(a1, b1) <= f(a2, b2).

This monotonicity requirement ensures that our operations respect the
special status of X as an unknown. For instance, an operation

Another way of looking at this is, if **any** value

On the other hand, if we only know that

**Function: **

(defun p4vm-suffix-args (args) (if (atom args) nil (cons (intern-in-package-of-symbol (concatenate 'string (symbol-name (car args)) "1") (car args)) (p4vm-suffix-args (cdr args)))))

**Function: **

(defun p4vm-4v-<=-args (args suff-args) (if (atom args) nil (cons (list '4v-<= (car args) (car suff-args)) (p4vm-4v-<=-args (cdr args) (cdr suff-args)))))

**Theorem: **

(defthm 4v-fix-is-monotonic (implies (and (4v-<= a a1)) (4v-<= (4v-fix a) (4v-fix a1))))

**Theorem: **

(defthm 4v-unfloat-is-monotonic (implies (and (4v-<= a a1)) (4v-<= (4v-unfloat a) (4v-unfloat a1))))

**Theorem: **

(defthm 4v-not-is-monotonic (implies (and (4v-<= a a1)) (4v-<= (4v-not a) (4v-not a1))))

**Theorem: **

(defthm 4v-xdet-is-monotonic (implies (and (4v-<= a a1)) (4v-<= (4v-xdet a) (4v-xdet a1))))

**Theorem: **

(defthm 4v-and-is-monotonic (implies (and (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-and a b) (4v-and a1 b1))))

**Theorem: **

(defthm 4v-or-is-monotonic (implies (and (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-or a b) (4v-or a1 b1))))

**Theorem: **

(defthm 4v-xor-is-monotonic (implies (and (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-xor a b) (4v-xor a1 b1))))

**Theorem: **

(defthm 4v-iff-is-monotonic (implies (and (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-iff a b) (4v-iff a1 b1))))

**Theorem: **

(defthm 4v-res-is-monotonic (implies (and (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-res a b) (4v-res a1 b1))))

**Theorem: **

(defthm 4v-ite-is-monotonic (implies (and (4v-<= c c1) (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-ite c a b) (4v-ite c1 a1 b1))))

**Theorem: **

(defthm 4v-ite*-is-monotonic (implies (and (4v-<= c c1) (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-ite* c a b) (4v-ite* c1 a1 b1))))

**Theorem: **

(defthm 4v-zif-is-monotonic (implies (and (4v-<= c c1) (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-zif c a b) (4v-zif c1 a1 b1))))

**Theorem: **

(defthm 4v-tristate-is-monotonic (implies (and (4v-<= c c1) (4v-<= a a1)) (4v-<= (4v-tristate c a) (4v-tristate c1 a1))))

**Theorem: **

(defthm 4v-pullup-is-monotonic (implies (and (4v-<= a a1)) (4v-<= (4v-pullup a) (4v-pullup a1))))

**Theorem: **

(defthm 4v-wand-is-monotonic (implies (and (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-wand a b) (4v-wand a1 b1))))

**Theorem: **

(defthm 4v-wor-is-monotonic (implies (and (4v-<= a a1) (4v-<= b b1)) (4v-<= (4v-wor a b) (4v-wor a1 b1))))

- 4v-sexpr-<=
- Extension of the four-valued lattice ordering to sexprs.