Equality check that, in FGL, splits an equivalence of SIMD packed integers into lane-by-lane equivalence checks.
(solve-lane-by-lane x y width) → *
The equivalence check of each of the lanes is done using the FGL
SAT config object
(defun solve-lane-by-lane (x y width) (declare (xargs :guard t)) (let ((__function__ 'solve-lane-by-lane)) (declare (ignorable __function__)) (equal x y)))
(defthm solve-lane-by-lane-impl (implies (and (syntaxp (posp width)) (check-integerp xintp x) (check-integerp yintp y)) (equal (solve-lane-by-lane x y width) (if (and (check-int-endp x-endp x) (check-int-endp y-endp y)) (equal x y) (b* ((config (syntax-bind config (g-concrete (solve-lane-by-lane-config))))) (and* (fgl-validity-check config (equal (loghead width x) (loghead width y))) (solve-lane-by-lane (logtail width x) (logtail width y) width)))))))