(a4vec-===*-aux a.upper a.lower b.upper b.lower) → (mv true not-false)
Function:
(defun a4vec-===*-aux (a.upper a.lower b.upper b.lower) (declare (xargs :guard (and (true-listp a.upper) (true-listp a.lower) (true-listp b.upper) (true-listp b.lower)))) (let ((__function__ 'a4vec-===*-aux)) (declare (ignorable __function__)) (b* (((mv buf bur buend) (gl::first/rest/end b.upper)) ((mv blf blr blend) (gl::first/rest/end b.lower)) ((mv auf aur auend) (gl::first/rest/end a.upper)) ((mv alf alr alend) (gl::first/rest/end a.lower)) ((mv true1 not-false1) (a4vec-===*-bit auf alf buf blf)) ((when (mbe :logic (and4 buend blend auend alend) :exec (and buend blend auend alend))) (mv true1 not-false1)) ((mv rest-true rest-not-false) (a4vec-===*-aux aur alr bur blr))) (mv (aig-and true1 rest-true) (aig-and not-false1 rest-not-false)))))
Theorem:
(defthm a4vec-===*-aux-of-list-fix-a.upper (equal (a4vec-===*-aux (list-fix a.upper) a.lower b.upper b.lower) (a4vec-===*-aux a.upper a.lower b.upper b.lower)))
Theorem:
(defthm a4vec-===*-aux-list-equiv-congruence-on-a.upper (implies (list-equiv a.upper a.upper-equiv) (equal (a4vec-===*-aux a.upper a.lower b.upper b.lower) (a4vec-===*-aux a.upper-equiv a.lower b.upper b.lower))) :rule-classes :congruence)
Theorem:
(defthm a4vec-===*-aux-of-list-fix-a.lower (equal (a4vec-===*-aux a.upper (list-fix a.lower) b.upper b.lower) (a4vec-===*-aux a.upper a.lower b.upper b.lower)))
Theorem:
(defthm a4vec-===*-aux-list-equiv-congruence-on-a.lower (implies (list-equiv a.lower a.lower-equiv) (equal (a4vec-===*-aux a.upper a.lower b.upper b.lower) (a4vec-===*-aux a.upper a.lower-equiv b.upper b.lower))) :rule-classes :congruence)
Theorem:
(defthm a4vec-===*-aux-of-list-fix-b.upper (equal (a4vec-===*-aux a.upper a.lower (list-fix b.upper) b.lower) (a4vec-===*-aux a.upper a.lower b.upper b.lower)))
Theorem:
(defthm a4vec-===*-aux-list-equiv-congruence-on-b.upper (implies (list-equiv b.upper b.upper-equiv) (equal (a4vec-===*-aux a.upper a.lower b.upper b.lower) (a4vec-===*-aux a.upper a.lower b.upper-equiv b.lower))) :rule-classes :congruence)
Theorem:
(defthm a4vec-===*-aux-of-list-fix-b.lower (equal (a4vec-===*-aux a.upper a.lower b.upper (list-fix b.lower)) (a4vec-===*-aux a.upper a.lower b.upper b.lower)))
Theorem:
(defthm a4vec-===*-aux-list-equiv-congruence-on-b.lower (implies (list-equiv b.lower b.lower-equiv) (equal (a4vec-===*-aux a.upper a.lower b.upper b.lower) (a4vec-===*-aux a.upper a.lower b.upper b.lower-equiv))) :rule-classes :congruence)