		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-logandc2-ss

Signature
(sv::aig-logandc2-ss a b) → andc2
Arguments: a — Guard (true-listp a).; b — Guard (true-listp b).
Returns: andc2 — Type (true-listp andc2).

Definitions and Theorems

Function: aig-logandc2-ss

(defun sv::aig-logandc2-ss (a b)
  (declare (xargs :guard (and (true-listp a) (true-listp b))))
  (let ((__function__ 'sv::aig-logandc2-ss))
    (declare (ignorable __function__))
    (b* (((mv af ar aend) (first/rest/end a))
         ((mv bf br bend) (first/rest/end b))
         (lsb (acl2::aig-andc2 af bf))
         ((when (and aend bend))
          (sv::aig-sterm lsb))
         (rest (sv::aig-logandc2-ss ar br)))
      (sv::aig-scons lsb rest))))

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

(defthm sv::true-listp-of-aig-logandc2-ss
  (b* ((andc2 (sv::aig-logandc2-ss a b)))
    (true-listp andc2))
  :rule-classes :type-prescription)

Theorem: aig-logandc2-ss-correct

(defthm sv::aig-logandc2-ss-correct
  (b* ((andc2 (sv::aig-logandc2-ss a b)))
    (and (equal (sv::aig-list->s andc2 env)
                (logandc2 (sv::aig-list->s a env)
                          (sv::aig-list->s b env))))))