		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-mod-ss-aux

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

Definitions and Theorems

Function: aabf-mod-ss-aux

(defun aabf-mod-ss-aux (a b not-b man)
 (declare (xargs :guard (and (true-listp a)
                             (true-listp b)
                             (true-listp not-b))))
 (declare (xargs :guard (and (aabflist-p a man)
                             (aabflist-p b man)
                             (aabflist-p not-b man))))
 (let ((__function__ 'aabf-mod-ss-aux))
  (declare (ignorable __function__))
  (mbe
   :logic
   (b* (((mv & mod man)
         (aabf-floor-ss-aux a b not-b man)))
     (mv mod man))
   :exec
   (b*
     (((mv first rest endp)
       (aabf-first/rest/end a))
      ((when endp)
       (aabf-nest (aabf-ite-bss first
                                (aabf-+-ss (aabf-false)
                                           (list (aabf-true))
                                           b)
                                nil)
                  man))
      (bound (aabf-integer-length-bound-s b man))
      ((mv rm man)
       (aabf-nest (aabf-scons first (aabf-mod-ss-aux rest b not-b))
                  man)))
    (aabf-nest
      (aabf-ite-bss
           (aabf-<-ss rm b)
           rm
           (aabf-loghead-ns bound (aabf-+-ss (aabf-true) not-b rm)))
      man)))))

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

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

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

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

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

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

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

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

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

(defthm aabf-eval-of-aabf-mod-ss-aux
 (b* (((mv m new-man)
       (aabf-mod-ss-aux a b not-b man)))
  (implies
   (and
      (aabflist-p a man)
      (aabflist-p b man)
      (aabflist-p not-b man)
      (and (< 0
              (bools->int (aabflist-eval b env man)))
           (equal (bools->int (aabflist-eval not-b env man))
                  (lognot (bools->int (aabflist-eval b env 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-aux

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