		Search-engine friendly clone of the ACL2 documentation.

4v-operations

4v-iff

Four-valued semantics for xnor gates.

(4v-iff a b) returns:

T when its inputs are Boolean and are the same, or
F when its inputs are Boolean and differ, or
X otherwise.

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

Definitions and Theorems

Function: 4v-iff$inline

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

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

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

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

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