		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-floor-ss-aux

Signature
(sv::aig-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: aig-floor-ss-aux

(defun sv::aig-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 (sv::aig-lognot-s b))))
 (let ((__function__ 'sv::aig-floor-ss-aux))
  (declare (ignorable __function__))
  (b* (((mv first rest endp)
        (first/rest/end a))
       (not-b (mbe :logic (sv::aig-lognot-s b)
                   :exec not-b)))
   (if endp (mv (sv::aig-sterm first)
                (sv::aig-ite-bss first (sv::aig-+-ss nil '(t) b)
                                 '(nil)))
    (b* (((mv rf rm)
          (sv::aig-floor-ss-aux rest b not-b))
         (rm (sv::aig-scons first rm))
         (less (sv::aig-<-ss rm b)))
      (mv (sv::aig-scons (acl2::aig-not less) rf)
          (sv::aig-ite-bss
               less rm
               (sv::aig-loghead-ns (integer-length-bound-s b)
                                   (sv::aig-+-ss t not-b rm)))))))))

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

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

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

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

Theorem: aig-floor-ss-aux-correct

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