		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

Aig-countones-aux

Signature
(aig-countones-aux x) → res
Arguments: x — Guard (true-listp x).
Returns: res — Type (true-listp res).

Definitions and Theorems

Function: aig-countones-aux

(defun aig-countones-aux (x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'aig-countones-aux))
    (declare (ignorable __function__))
    (if (atom x)
        nil
      (b* ((rest (aig-countones-aux (cdr x))))
        (aig-+-ss (car x) nil rest)))))

Theorem: true-listp-of-aig-countones-aux

(defthm true-listp-of-aig-countones-aux
  (b* ((res (aig-countones-aux x)))
    (true-listp res))
  :rule-classes :rewrite)

Theorem: aig-countones-aux-correct

(defthm aig-countones-aux-correct
  (b* nil
    (equal (aig-list->s (aig-countones-aux x) env)
           (logcount (aig-list->u x env)))))

Theorem: aig-countones-aux-of-list-fix-x

(defthm aig-countones-aux-of-list-fix-x
  (equal (aig-countones-aux (list-fix x))
         (aig-countones-aux x)))

Theorem: aig-countones-aux-list-equiv-congruence-on-x

(defthm aig-countones-aux-list-equiv-congruence-on-x
  (implies (list-equiv x x-equiv)
           (equal (aig-countones-aux x)
                  (aig-countones-aux x-equiv)))
  :rule-classes :congruence)