		Search-engine friendly clone of the ACL2 documentation.

Undocumented

4v-equiv

Equivalence of four-valued constants, i.e., 4vps.

X === Y in the sense of four-valued objects if they fix to the same 4vp. That is, except for (4vf), (4vz), and (4vt), all objects are equivalent to (4vx) under this relationship.

Function: 4v-equiv

(defun 4v-equiv (x y)
  (and (equal (4v-fix x) (4v-fix y))))

Definitions and Theorems

Function: 4v-equiv

(defun 4v-equiv (x y)
  (and (equal (4v-fix x) (4v-fix y))))

Theorem: 4v-equiv-is-an-equivalence

(defthm 4v-equiv-is-an-equivalence
  (and (booleanp (4v-equiv x y))
       (4v-equiv x x)
       (implies (4v-equiv x y) (4v-equiv y x))
       (implies (and (4v-equiv x y) (4v-equiv y z))
                (4v-equiv x z)))
  :rule-classes (:equivalence))