		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-floor-ss

Signature
(sv::aig-floor-ss a b) → f
Arguments: a — Guard (true-listp a).; b — Guard (true-listp b).
Returns: f — Type (true-listp f).

Definitions and Theorems

Function: aig-floor-ss

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

Theorem: true-listp-of-aig-floor-ss

(defthm sv::true-listp-of-aig-floor-ss
  (b* ((f (sv::aig-floor-ss a b)))
    (true-listp f))
  :rule-classes :type-prescription)

Theorem: aig-floor-ss-correct

(defthm sv::aig-floor-ss-correct
  (b* ((f (sv::aig-floor-ss a b)))
    (and (equal (sv::aig-list->s f env)
                (floor (sv::aig-list->s a env)
                       (sv::aig-list->s b env))))))