(aig-overlap-width-ss-aux rev-pos pos-len x y width) → *
Function:
(defun aig-overlap-width-ss-aux (rev-pos pos-len x y width) (declare (xargs :guard (and (true-listp rev-pos) (true-listp x) (true-listp y) (posp width) (equal pos-len (len rev-pos))))) (let ((__function__ 'aig-overlap-width-ss-aux)) (declare (ignorable __function__)) (b* ((rev-pos (llist-fix rev-pos)) (y (llist-fix y)) (x (llist-fix x)) (width (lposfix width)) ((when (atom rev-pos)) y) (pos-len (1- (mbe :logic (len rev-pos) :exec pos-len))) ((when (eq (car rev-pos) nil)) (aig-overlap-width-ss-aux (cdr rev-pos) pos-len x y width)) (pos-too-large (mbe :logic (<= width (ash 1 pos-len)) :exec (or (< (integer-length width) pos-len) (<= width (ash 1 pos-len))))) (rest1 (if pos-too-large x (b* ((nshifted (ash 1 pos-len))) (aig-logapp-nss nshifted x (aig-overlap-width-ss-aux (cdr rev-pos) pos-len (aig-logtail-ns nshifted x) (aig-logtail-ns nshifted y) (- width nshifted)))))) ((when (eq (car rev-pos) t)) rest1) (rest0 (aig-overlap-width-ss-aux (cdr rev-pos) pos-len x y width))) (aig-ite-bss (car rev-pos) rest1 rest0))))
Theorem:
(defthm aig-overlap-width-ss-aux-correct (implies (and (signed-byte-p (pos-fix width) (aig-list->s x env)) (signed-byte-p (pos-fix width) (aig-list->s y env))) (equal (aig-list->s (aig-overlap-width-ss-aux rev-pos pos-len x y width) env) (b* ((pos (aig-list->u (rev rev-pos) env))) (logext width (logapp pos (aig-list->s x env) (logtail pos (aig-list->s y env))))))))
Theorem:
(defthm aig-overlap-width-ss-aux-of-list-fix-rev-pos (equal (aig-overlap-width-ss-aux (list-fix rev-pos) pos-len x y width) (aig-overlap-width-ss-aux rev-pos pos-len x y width)))
Theorem:
(defthm aig-overlap-width-ss-aux-list-equiv-congruence-on-rev-pos (implies (list-equiv rev-pos rev-pos-equiv) (equal (aig-overlap-width-ss-aux rev-pos pos-len x y width) (aig-overlap-width-ss-aux rev-pos-equiv pos-len x y width))) :rule-classes :congruence)
Theorem:
(defthm aig-overlap-width-ss-aux-of-list-fix-x (equal (aig-overlap-width-ss-aux rev-pos pos-len (list-fix x) y width) (aig-overlap-width-ss-aux rev-pos pos-len x y width)))
Theorem:
(defthm aig-overlap-width-ss-aux-list-equiv-congruence-on-x (implies (list-equiv x x-equiv) (equal (aig-overlap-width-ss-aux rev-pos pos-len x y width) (aig-overlap-width-ss-aux rev-pos pos-len x-equiv y width))) :rule-classes :congruence)
Theorem:
(defthm aig-overlap-width-ss-aux-of-list-fix-y (equal (aig-overlap-width-ss-aux rev-pos pos-len x (list-fix y) width) (aig-overlap-width-ss-aux rev-pos pos-len x y width)))
Theorem:
(defthm aig-overlap-width-ss-aux-list-equiv-congruence-on-y (implies (list-equiv y y-equiv) (equal (aig-overlap-width-ss-aux rev-pos pos-len x y width) (aig-overlap-width-ss-aux rev-pos pos-len x y-equiv width))) :rule-classes :congruence)
Theorem:
(defthm aig-overlap-width-ss-aux-of-pos-fix-width (equal (aig-overlap-width-ss-aux rev-pos pos-len x y (pos-fix width)) (aig-overlap-width-ss-aux rev-pos pos-len x y width)))
Theorem:
(defthm aig-overlap-width-ss-aux-pos-equiv-congruence-on-width (implies (pos-equiv width width-equiv) (equal (aig-overlap-width-ss-aux rev-pos pos-len x y width) (aig-overlap-width-ss-aux rev-pos pos-len x y width-equiv))) :rule-classes :congruence)