		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-rem-ss

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

Definitions and Theorems

Function: aig-rem-ss

(defun sv::aig-rem-ss (a b)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (let ((__function__ 'sv::aig-rem-ss))
    (declare (ignorable __function__))
    (sv::aig-ite-bss
         (sv::aig-=-ss b nil)
         (llist-fix a)
         (b* (((mv & babs bneg)
               (sv::aig-sign-abs-not-s b))
              ((mv asign aabs &)
               (sv::aig-sign-abs-not-s a))
              (m (sv::aig-mod-ss-aux aabs babs bneg)))
           (sv::aig-logext-ns
                (integer-length-bound-s b)
                (sv::aig-ite-bss asign (sv::aig-unary-minus-s m)
                                 m))))))

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

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

Theorem: aig-rem-ss-correct

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