Make sure there is no pair of bits with Xi == 0 while Yi == 1.
(a4vec-syntactic-3vec-p-rec x y) → bool
Function:
(defun a4vec-syntactic-3vec-p-rec (x y) (declare (xargs :guard (and (true-listp x) (true-listp y)))) (let ((__function__ 'a4vec-syntactic-3vec-p-rec)) (declare (ignorable __function__)) (b* (((mv xf xr xe) (gl::first/rest/end x)) ((mv yf yr ye) (gl::first/rest/end y))) (and (or (eq xf t) (eq yf nil) (hons-equal xf yf)) (if (and xe ye) t (a4vec-syntactic-3vec-p-rec xr yr))))))
Theorem:
(defthm a4vec-syntactic-3vec-p-rec-correct (implies (a4vec-syntactic-3vec-p-rec x y) (equal (logand (aig-list->s y env) (lognot (aig-list->s x env))) 0)))
Theorem:
(defthm a4vec-syntactic-3vec-p-rec-of-list-fix-x (equal (a4vec-syntactic-3vec-p-rec (list-fix x) y) (a4vec-syntactic-3vec-p-rec x y)))
Theorem:
(defthm a4vec-syntactic-3vec-p-rec-list-equiv-congruence-on-x (implies (list-equiv x x-equiv) (equal (a4vec-syntactic-3vec-p-rec x y) (a4vec-syntactic-3vec-p-rec x-equiv y))) :rule-classes :congruence)
Theorem:
(defthm a4vec-syntactic-3vec-p-rec-of-list-fix-y (equal (a4vec-syntactic-3vec-p-rec x (list-fix y)) (a4vec-syntactic-3vec-p-rec x y)))
Theorem:
(defthm a4vec-syntactic-3vec-p-rec-list-equiv-congruence-on-y (implies (list-equiv y y-equiv) (equal (a4vec-syntactic-3vec-p-rec x y) (a4vec-syntactic-3vec-p-rec x y-equiv))) :rule-classes :congruence)