		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))