		Search-engine friendly clone of the ACL2 documentation.

Aig-symbolic-arithmetic

Sv::aig-logand-ssss

Signature
(sv::aig-logand-ssss a b c d) → and
Arguments: a — Guard (true-listp a).; b — Guard (true-listp b).; c — Guard (true-listp c).; d — Guard (true-listp d).
Returns: and — Type (true-listp and).

Definitions and Theorems

Function: aig-logand-ssss

(defun sv::aig-logand-ssss (a b c d)
  (declare (xargs :guard (and (true-listp a)
                              (true-listp b)
                              (true-listp c)
                              (true-listp d))))
  (let ((__function__ 'sv::aig-logand-ssss))
    (declare (ignorable __function__))
    (b* (((mv af ar aend) (first/rest/end a))
         ((mv bf br bend) (first/rest/end b))
         ((mv cf cr cend) (first/rest/end c))
         ((mv df dr dend) (first/rest/end d))
         (lsb (acl2::aig-and af bf cf df))
         ((when (and aend bend cend dend))
          (sv::aig-sterm lsb))
         (rest (sv::aig-logand-ssss ar br cr dr)))
      (sv::aig-scons lsb rest))))

Theorem: true-listp-of-aig-logand-ssss

(defthm sv::true-listp-of-aig-logand-ssss
  (b* ((and (sv::aig-logand-ssss a b c d)))
    (true-listp and))
  :rule-classes :type-prescription)

Theorem: aig-logand-ssss-correct

(defthm sv::aig-logand-ssss-correct
 (b* ((and (sv::aig-logand-ssss a b c d)))
  (and (equal (sv::aig-list->s and env)
              (logand (sv::aig-list->s a env)
                      (logand (sv::aig-list->s b env)
                              (logand (sv::aig-list->s c env)
                                      (sv::aig-list->s d env))))))))