Symbolic function that replaces
(aig-overlap-width-ss pos x y width) → *
Symbolically computes:
(logext width (logapp pos x (logtail pos y)))
where all variables except
Function:
(defun aig-overlap-width-ss (pos x y width) (declare (xargs :guard (and (true-listp pos) (true-listp x) (true-listp y) (posp width)))) (let ((__function__ 'aig-overlap-width-ss)) (declare (ignorable __function__)) (b* ((width (lposfix width)) (same-signp (hons-equal (aig-sign-s x) (aig-sign-s y))) (width (if same-signp (min (+ 1 (max (len x) (len y))) width) width)) (y-ext (aig-logext-ns width y))) (aig-ite-bss (aig-sign-s pos) y-ext (b* ((rev-pos (cdr (rev pos)))) (aig-overlap-width-ss-aux rev-pos (len rev-pos) (aig-logext-ns width x) y-ext width))))))
Theorem:
(defthm aig-overlap-width-ss-correct (equal (aig-list->s (aig-overlap-width-ss pos x y width) env) (b* ((pos (aig-list->s pos env))) (logext width (logapp pos (aig-list->s x env) (logtail pos (aig-list->s y env)))))))
Theorem:
(defthm aig-overlap-width-ss-of-list-fix-pos (equal (aig-overlap-width-ss (list-fix pos) x y width) (aig-overlap-width-ss pos x y width)))
Theorem:
(defthm aig-overlap-width-ss-list-equiv-congruence-on-pos (implies (list-equiv pos pos-equiv) (equal (aig-overlap-width-ss pos x y width) (aig-overlap-width-ss pos-equiv x y width))) :rule-classes :congruence)
Theorem:
(defthm aig-overlap-width-ss-of-list-fix-x (equal (aig-overlap-width-ss pos (list-fix x) y width) (aig-overlap-width-ss pos x y width)))
Theorem:
(defthm aig-overlap-width-ss-list-equiv-congruence-on-x (implies (list-equiv x x-equiv) (equal (aig-overlap-width-ss pos x y width) (aig-overlap-width-ss pos x-equiv y width))) :rule-classes :congruence)
Theorem:
(defthm aig-overlap-width-ss-of-list-fix-y (equal (aig-overlap-width-ss pos x (list-fix y) width) (aig-overlap-width-ss pos x y width)))
Theorem:
(defthm aig-overlap-width-ss-list-equiv-congruence-on-y (implies (list-equiv y y-equiv) (equal (aig-overlap-width-ss pos x y width) (aig-overlap-width-ss pos x y-equiv width))) :rule-classes :congruence)
Theorem:
(defthm aig-overlap-width-ss-of-pos-fix-width (equal (aig-overlap-width-ss pos x y (pos-fix width)) (aig-overlap-width-ss pos x y width)))
Theorem:
(defthm aig-overlap-width-ss-pos-equiv-congruence-on-width (implies (pos-equiv width width-equiv) (equal (aig-overlap-width-ss pos x y width) (aig-overlap-width-ss pos x y width-equiv))) :rule-classes :congruence)