		Search-engine friendly clone of the ACL2 documentation.

4v-operations

4v-and

Four-valued semantics for and gates.

(4v-and a b) returns:

F when either input is F, or
X when either input is X/Z, or
T when both inputs are T.

See 4v-unfloat for an explanation of the Z case.

Definitions and Theorems

Function: 4v-and$inline

(defun 4v-and$inline (a b)
       (declare (xargs :guard t))
       (mbe :logic (4vcases a (t (4v-unfloat b))
                            (f (4vf))
                            (& (4vcases b (f (4vf)) (& (4vx)))))
            :exec (cond ((or (eq a (4vf)) (eq b (4vf))) (4vf))
                        ((and (eq a (4vt)) (eq b (4vt))) (4vt))
                        (t (4vx)))))

Theorem: 4v-equiv-implies-equal-4v-and-2

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

Theorem: 4v-equiv-implies-equal-4v-and-1

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