		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-mod-ss

Signature
(bfr-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: bfr-mod-ss

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

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

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

Theorem: bfr-mod-ss-correct

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

Theorem: bfr-mod-ss-deps

(defthm bfr-mod-ss-deps
  (b* ((m (bfr-mod-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 m))))))