		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-*-ss

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

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

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

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

Theorem: aig-*-ss-correct

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