		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-mod-ss

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

Definitions and Theorems

Function: aig-mod-ss

(defun sv::aig-mod-ss (a b)
 (declare (xargs :guard (and (true-listp a) (true-listp b))))
 (let ((__function__ 'sv::aig-mod-ss))
  (declare (ignorable __function__))
  (sv::aig-ite-bss
   (sv::aig-=-ss b nil)
   (llist-fix a)
   (sv::aig-logext-ns
        (integer-length-bound-s b)
        (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))
             (m (sv::aig-mod-ss-aux anorm babs bneg)))
          (sv::aig-ite-bss bsign (sv::aig-unary-minus-s m)
                           m))))))

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

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

Theorem: aig-mod-ss-correct

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