		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-floor-ss-aux

Signature
(bfr-floor-ss-aux a b not-b) → (mv f m)
Arguments: a — Guard (true-listp a).; b — Guard (true-listp b).; not-b — Guard (true-listp not-b).
Returns: f — Type (true-listp f).; m — Type (true-listp m).

Definitions and Theorems

Function: bfr-floor-ss-aux

(defun bfr-floor-ss-aux (a b not-b)
 (declare (xargs :guard (and (true-listp a)
                             (true-listp b)
                             (true-listp not-b))))
 (declare (xargs :guard (equal not-b (bfr-lognot-s b))))
 (let ((__function__ 'bfr-floor-ss-aux))
  (declare (ignorable __function__))
  (b* (((mv first rest endp)
        (first/rest/end a))
       (not-b (mbe :logic (bfr-lognot-s b)
                   :exec not-b)))
   (if endp (mv (bfr-sterm first)
                (bfr-ite-bss first (bfr-+-ss nil '(t) b)
                             '(nil)))
    (b* (((mv rf rm)
          (bfr-floor-ss-aux rest b not-b))
         (rm (bfr-scons first rm))
         (less (bfr-<-ss rm b)))
      (mv (bfr-scons (bfr-not less) rf)
          (bfr-ite-bss less rm
                       (bfr-loghead-ns (integer-length-bound-s b)
                                       (bfr-+-ss t not-b rm)))))))))

Theorem: true-listp-of-bfr-floor-ss-aux.f

(defthm true-listp-of-bfr-floor-ss-aux.f
  (b* (((mv acl2::?f acl2::?m)
        (bfr-floor-ss-aux a b not-b)))
    (true-listp f))
  :rule-classes :type-prescription)

Theorem: true-listp-of-bfr-floor-ss-aux.m

(defthm true-listp-of-bfr-floor-ss-aux.m
  (b* (((mv acl2::?f acl2::?m)
        (bfr-floor-ss-aux a b not-b)))
    (true-listp m))
  :rule-classes :type-prescription)

Theorem: bfr-floor-ss-aux-correct

(defthm bfr-floor-ss-aux-correct
  (b* (((mv f m) (bfr-floor-ss-aux a b not-b)))
    (implies (< 0 (bfr-list->s b env))
             (and (equal (bfr-list->s f env)
                         (floor (bfr-list->s a env)
                                (bfr-list->s b env)))
                  (equal (bfr-list->s m env)
                         (mod (bfr-list->s a env)
                              (bfr-list->s b env)))))))

Theorem: bfr-floor-ss-aux-deps

(defthm bfr-floor-ss-aux-deps
  (b* (((mv f m) (bfr-floor-ss-aux a b not-b)))
    (implies (and (not (pbfr-list-depends-on varname param a))
                  (not (pbfr-list-depends-on varname param b))
                  (not (pbfr-list-depends-on varname param not-b)))
             (and (not (pbfr-list-depends-on varname param f))
                  (not (pbfr-list-depends-on varname param m))))))