(sv::aig-mod-ss-aux a b not-b) → m
Function:
(defun sv::aig-mod-ss-aux (a b not-b) (declare (xargs :guard (and (true-listp a) (true-listp b) (true-listp not-b)))) (declare (xargs :guard (equal not-b (sv::aig-lognot-s b)))) (let ((__function__ 'sv::aig-mod-ss-aux)) (declare (ignorable __function__)) (mbe :logic (non-exec (mv-nth 1 (sv::aig-floor-ss-aux a b not-b))) :exec (b* (((mv first rest endp) (first/rest/end a)) (not-b (mbe :logic (sv::aig-lognot-s b) :exec not-b)) ((when endp) (sv::aig-ite-bss first (sv::aig-+-ss nil '(t) b) '(nil))) (rm (sv::aig-mod-ss-aux rest b not-b)) (rm (sv::aig-scons first rm)) (less (sv::aig-<-ss rm b))) (sv::aig-ite-bss less rm (sv::aig-loghead-ns (integer-length-bound-s b) (sv::aig-+-ss t not-b rm)))))))
Theorem:
(defthm sv::true-listp-of-aig-mod-ss-aux (b* ((m (sv::aig-mod-ss-aux a b not-b))) (true-listp m)) :rule-classes :type-prescription)
Theorem:
(defthm sv::aig-mod-ss-aux-correct (b* ((m (sv::aig-mod-ss-aux a b not-b))) (implies (< 0 (sv::aig-list->s b env)) (and (equal (sv::aig-list->s m env) (mod (sv::aig-list->s a env) (sv::aig-list->s b env)))))))