		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

Aig-iszero-s

Determines whether a signed vector of AIGs is equal to 0.

Signature
(aig-iszero-s a) → res
Arguments: a — Guard (true-listp a).
Returns: res — aig.

Definitions and Theorems

Function: aig-iszero-s

(defun aig-iszero-s (a)
  (declare (xargs :guard (true-listp a)))
  (let ((__function__ 'aig-iszero-s))
    (declare (ignorable __function__))
    (b* (((mv first rest end)
          (gl::first/rest/end a))
         ((when end) (aig-not first)))
      (aig-and (aig-not first)
               (aig-iszero-s rest)))))

Theorem: aig-iszero-s-correct

(defthm aig-iszero-s-correct
  (equal (aig-eval (aig-iszero-s a) env)
         (equal (aig-list->s a env) 0)))

Theorem: aig-iszero-s-of-list-fix-a

(defthm aig-iszero-s-of-list-fix-a
  (equal (aig-iszero-s (list-fix a))
         (aig-iszero-s a)))

Theorem: aig-iszero-s-list-equiv-congruence-on-a

(defthm aig-iszero-s-list-equiv-congruence-on-a
  (implies (list-equiv a a-equiv)
           (equal (aig-iszero-s a)
                  (aig-iszero-s a-equiv)))
  :rule-classes :congruence)