Unusual semantics for a multiplexor, used mainly to implement composition features in esim
A ZIF module is in some ways similar to a pass-gate based multiplexor, but is probably not the sort of thing you would actually want to use to model a mux. It is very similar to an 4v-ite* but does not 4v-unfloat its inputs. We include this mainly as a way to implement experimental composition features in esim.
(defun 4v-zif (c a b) (declare (xargs :guard t)) (mbe :logic (4vcases c (t (4v-fix a)) (f (4v-fix b)) (& (4vx))) :exec (cond ((eq c (4vt)) (4v-fix a)) ((eq c (4vf)) (4v-fix b)) (t (4vx)))))
(defthm 4v-equiv-implies-equal-4v-zif-3 (implies (4v-equiv b b-equiv) (equal (4v-zif c a b) (4v-zif c a b-equiv))) :rule-classes (:congruence))
(defthm 4v-equiv-implies-equal-4v-zif-2 (implies (4v-equiv a a-equiv) (equal (4v-zif c a b) (4v-zif c a-equiv b))) :rule-classes (:congruence))
(defthm 4v-equiv-implies-equal-4v-zif-1 (implies (4v-equiv c c-equiv) (equal (4v-zif c a b) (4v-zif c-equiv a b))) :rule-classes (:congruence))