(aabf-floor-ss a b man) → (mv f new-man)
Function:
(defun aabf-floor-ss (a b man) (declare (xargs :guard (and (true-listp a) (true-listp b)))) (declare (xargs :guard (and (aabflist-p a man) (aabflist-p b man)))) (let ((__function__ 'aabf-floor-ss)) (declare (ignorable __function__)) (b* (((mv bsign babs bneg man) (aabf-sign-abs-not-s b man)) ((mv anorm man) (aabf-nest (aabf-ite-bss bsign (aabf-unary-minus-s a) a) man)) ((mv f & man) (aabf-floor-ss-aux anorm babs bneg man))) (aabf-nest (aabf-ite-bss (aabf-=-ss b nil) nil f) man))))
Theorem:
(defthm trivial-theorem-about-aabf-floor-ss (b* nil (b* ((?ignore (aabf-floor-ss a b man))) t)) :rule-classes nil)
Theorem:
(defthm true-listp-of-aabf-floor-ss.f (b* (((mv acl2::?f ?new-man) (aabf-floor-ss a b man))) (true-listp f)) :rule-classes :type-prescription)
Theorem:
(defthm aabf-extension-p-of-aabf-floor-ss (b* (((mv acl2::?f ?new-man) (aabf-floor-ss a b man))) (aabf-extension-p new-man man)))
Theorem:
(defthm aabf-p-of-aabf-floor-ss (b* (((mv f new-man) (aabf-floor-ss a b man))) (implies (and (aabflist-p a man) (aabflist-p b man)) (and (aabflist-p f new-man)))))
Theorem:
(defthm aabf-eval-of-aabf-floor-ss (b* (((mv f new-man) (aabf-floor-ss a b man))) (implies (and (aabflist-p a man) (aabflist-p b 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))))))))
Theorem:
(defthm aabf-pred-of-aabf-floor-ss (b* (((mv f new-man) (aabf-floor-ss a b man))) (implies (and (aabflist-p a man) (aabflist-p b man) (aabflist-pred a man) (aabflist-pred b man)) (and (aabflist-pred f new-man)))))