		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-mod-ss

Signature
(aabf-mod-ss a b man) → (mv m new-man)
Arguments: a — Guard (true-listp a).; b — Guard (true-listp b).

Definitions and Theorems

Function: aabf-mod-ss

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

Theorem: trivial-theorem-about-aabf-mod-ss

(defthm trivial-theorem-about-aabf-mod-ss
  (b* nil
    (b* ((?ignore (aabf-mod-ss a b man)))
      t))
  :rule-classes nil)

Theorem: true-listp-of-aabf-mod-ss.m

(defthm true-listp-of-aabf-mod-ss.m
  (b* (((mv acl2::?m ?new-man)
        (aabf-mod-ss a b man)))
    (true-listp m))
  :rule-classes :type-prescription)

Theorem: aabf-extension-p-of-aabf-mod-ss

(defthm aabf-extension-p-of-aabf-mod-ss
  (b* (((mv acl2::?m ?new-man)
        (aabf-mod-ss a b man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-mod-ss

(defthm aabf-p-of-aabf-mod-ss
  (b* (((mv m new-man) (aabf-mod-ss a b man)))
    (implies (and (aabflist-p a man)
                  (aabflist-p b man))
             (and (aabflist-p m new-man)))))

Theorem: aabf-eval-of-aabf-mod-ss

(defthm aabf-eval-of-aabf-mod-ss
 (b* (((mv m new-man) (aabf-mod-ss a b man)))
  (implies
       (and (aabflist-p a man)
            (aabflist-p b man))
       (and (equal (bools->int (aabflist-eval m env new-man))
                   (mod (bools->int (aabflist-eval a env man))
                        (bools->int (aabflist-eval b env man))))))))

Theorem: aabf-pred-of-aabf-mod-ss

(defthm aabf-pred-of-aabf-mod-ss
  (b* (((mv m new-man) (aabf-mod-ss a b man)))
    (implies (and (aabflist-p a man)
                  (aabflist-p b man)
                  (aabflist-pred a man)
                  (aabflist-pred b man))
             (and (aabflist-pred m new-man)))))