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