		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Bfr-*-ss

Signature
(bfr-*-ss v1 v2) → prod
Arguments: v1 — Guard (true-listp v1).; v2 — Guard (true-listp v2).
Returns: prod — Type (true-listp prod).

Definitions and Theorems

Function: bfr-*-ss

(defun bfr-*-ss (v1 v2)
  (declare (xargs :guard (and (true-listp v1) (true-listp v2))))
  (let ((__function__ 'bfr-*-ss))
    (declare (ignorable __function__))
    (b* (((mv dig1 rest end1)
          (first/rest/end v1))
         ((when end1)
          (bfr-ite-bss dig1 (bfr-unary-minus-s v2)
                       nil))
         (rest (bfr-*-ss rest v2)))
      (bfr-+-ss nil (bfr-ite-bss dig1 v2 nil)
                (bfr-scons nil rest)))))

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

(defthm true-listp-of-bfr-*-ss
  (b* ((prod (bfr-*-ss v1 v2)))
    (true-listp prod))
  :rule-classes :type-prescription)

Theorem: bfr-*-ss-correct

(defthm bfr-*-ss-correct
  (b* ((prod (bfr-*-ss v1 v2)))
    (and (equal (bfr-list->s prod env)
                (* (bfr-list->s v1 env)
                   (bfr-list->s v2 env))))))

Theorem: bfr-*-ss-deps

(defthm bfr-*-ss-deps
 (b* ((prod (bfr-*-ss v1 v2)))
   (implies (and (not (pbfr-list-depends-on varname param v1))
                 (not (pbfr-list-depends-on varname param v2)))
            (and (not (pbfr-list-depends-on varname param prod))))))