(aabf-floor-ss-aux a b not-b man) → (mv f m new-man)
Function:
(defun aabf-floor-ss-aux (a b not-b man) (declare (xargs :guard (and (true-listp a) (true-listp b) (true-listp not-b)))) (declare (xargs :guard (and (aabflist-p a man) (aabflist-p b man) (aabflist-p not-b man)))) (let ((__function__ 'aabf-floor-ss-aux)) (declare (ignorable __function__)) (b* (((mv first rest endp) (aabf-first/rest/end a))) (if endp (b* ((floor (list first)) ((mv mod man) (aabf-nest (aabf-ite-bss first (aabf-+-ss (aabf-false) (list (aabf-true)) b) nil) man))) (mv floor mod man)) (b* ((bound (aabf-integer-length-bound-s b man)) ((mv rf rm man) (aabf-floor-ss-aux rest b not-b man)) (rm (aabf-scons first rm)) ((mv less man) (aabf-<-ss rm b man)) (floor (aabf-scons (aabf-not less man) rf)) ((mv mod man) (aabf-nest (aabf-ite-bss less rm (aabf-loghead-ns bound (aabf-+-ss (aabf-true) not-b rm))) man))) (mv floor mod man))))))
Theorem:
(defthm trivial-theorem-about-aabf-floor-ss-aux (b* nil (b* ((?ignore (aabf-floor-ss-aux a b not-b man))) t)) :rule-classes nil)
Theorem:
(defthm true-listp-of-aabf-floor-ss-aux.f (b* (((mv acl2::?f acl2::?m ?new-man) (aabf-floor-ss-aux a b not-b man))) (true-listp f)) :rule-classes :type-prescription)
Theorem:
(defthm true-listp-of-aabf-floor-ss-aux.m (b* (((mv acl2::?f acl2::?m ?new-man) (aabf-floor-ss-aux a b not-b man))) (true-listp m)) :rule-classes :type-prescription)
Theorem:
(defthm aabf-extension-p-of-aabf-floor-ss-aux (b* (((mv acl2::?f acl2::?m ?new-man) (aabf-floor-ss-aux a b not-b man))) (aabf-extension-p new-man man)))
Theorem:
(defthm aabf-p-of-aabf-floor-ss-aux (b* (((mv f m new-man) (aabf-floor-ss-aux a b not-b man))) (implies (and (aabflist-p a man) (aabflist-p b man) (aabflist-p not-b man)) (and (aabflist-p f new-man) (aabflist-p m new-man)))))
Theorem:
(defthm aabf-eval-of-aabf-floor-ss-aux (b* (((mv f m new-man) (aabf-floor-ss-aux a b not-b man))) (implies (and (aabflist-p a man) (aabflist-p b man) (aabflist-p not-b man) (and (< 0 (bools->int (aabflist-eval b env man))) (equal (bools->int (aabflist-eval not-b env man)) (lognot (bools->int (aabflist-eval b env man)))))) (and (equal (bools->int (aabflist-eval f env new-man)) (floor (bools->int (aabflist-eval a env man)) (bools->int (aabflist-eval b env man)))) (equal (bools->int (aabflist-eval m env new-man)) (mod (bools->int (aabflist-eval a env man)) (bools->int (aabflist-eval b env man))))))))
Theorem:
(defthm aabf-pred-of-aabf-floor-ss-aux (b* (((mv f m new-man) (aabf-floor-ss-aux a b not-b man))) (implies (and (aabflist-p a man) (aabflist-p b man) (aabflist-p not-b man) (aabflist-pred a man) (aabflist-pred b man) (aabflist-pred not-b man)) (and (aabflist-pred f new-man) (aabflist-pred m new-man)))))