		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-truncate-ss

Signature
(bfr-truncate-ss a b) → tr
Arguments: a — Guard (true-listp a).; b — Guard (true-listp b).
Returns: tr — Type (true-listp tr).

Definitions and Theorems

Function: bfr-truncate-ss

(defun bfr-truncate-ss (a b)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (let ((__function__ 'bfr-truncate-ss))
    (declare (ignorable __function__))
    (bfr-ite-bss (bfr-=-ss b nil)
                 nil
                 (b* (((mv bsign babs bneg)
                       (bfr-sign-abs-not-s b))
                      ((mv asign aabs &)
                       (bfr-sign-abs-not-s a))
                      ((mv f &)
                       (bfr-floor-ss-aux aabs babs bneg)))
                   (bfr-ite-bss (bfr-xor bsign asign)
                                (bfr-unary-minus-s f)
                                f)))))

Theorem: true-listp-of-bfr-truncate-ss

(defthm true-listp-of-bfr-truncate-ss
  (b* ((tr (bfr-truncate-ss a b)))
    (true-listp tr))
  :rule-classes :type-prescription)

Theorem: bfr-truncate-ss-correct

(defthm bfr-truncate-ss-correct
  (b* ((tr (bfr-truncate-ss a b)))
    (and (equal (bfr-list->s tr env)
                (truncate (bfr-list->s a env)
                          (bfr-list->s b env))))))

Theorem: bfr-truncate-ss-deps

(defthm bfr-truncate-ss-deps
  (b* ((tr (bfr-truncate-ss a b)))
    (implies (and (not (pbfr-list-depends-on varname param a))
                  (not (pbfr-list-depends-on varname param b)))
             (and (not (pbfr-list-depends-on varname param tr))))))