		Search-engine friendly clone of the ACL2 documentation.

Symbolic-arithmetic

Aabf-*-ss

Signature
(aabf-*-ss v1 v2 man) → (mv prod new-man)
Arguments: v1 — Guard (true-listp v1).; v2 — Guard (true-listp v2).

Definitions and Theorems

Function: aabf-*-ss

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

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

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

Theorem: true-listp-of-aabf-*-ss.prod

(defthm true-listp-of-aabf-*-ss.prod
  (b* (((mv ?prod ?new-man)
        (aabf-*-ss v1 v2 man)))
    (true-listp prod))
  :rule-classes :type-prescription)

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

(defthm aabf-extension-p-of-aabf-*-ss
  (b* (((mv ?prod ?new-man)
        (aabf-*-ss v1 v2 man)))
    (aabf-extension-p new-man man)))

Theorem: aabf-p-of-aabf-*-ss

(defthm aabf-p-of-aabf-*-ss
  (b* (((mv prod new-man)
        (aabf-*-ss v1 v2 man)))
    (implies (and (aabflist-p v1 man)
                  (aabflist-p v2 man))
             (and (aabflist-p prod new-man)))))

Theorem: aabf-eval-of-aabf-*-ss

(defthm aabf-eval-of-aabf-*-ss
 (b* (((mv prod new-man)
       (aabf-*-ss v1 v2 man)))
   (implies
        (and (aabflist-p v1 man)
             (aabflist-p v2 man))
        (and (equal (bools->int (aabflist-eval prod env new-man))
                    (* (bools->int (aabflist-eval v1 env man))
                       (bools->int (aabflist-eval v2 env man))))))))

Theorem: aabf-pred-of-aabf-*-ss

(defthm aabf-pred-of-aabf-*-ss
  (b* (((mv prod new-man)
        (aabf-*-ss v1 v2 man)))
    (implies (and (aabflist-p v1 man)
                  (aabflist-p v2 man)
                  (aabflist-pred v1 man)
                  (aabflist-pred v2 man))
             (and (aabflist-pred prod new-man)))))