		Search-engine friendly clone of the ACL2 documentation.

A4vec-operations

Aig-onehot-aux

Signature
(aig-onehot-aux x) → (mv zero one)
Arguments: x — Guard (true-listp x).

Definitions and Theorems

Function: aig-onehot-aux

(defun aig-onehot-aux (x)
  (declare (xargs :guard (true-listp x)))
  (let ((__function__ 'aig-onehot-aux))
    (declare (ignorable __function__))
    (b* (((when (atom x)) (mv t nil))
         ((mv zero one)
          (aig-onehot-aux (cdr x))))
      (mv (aig-and zero (aig-not (car x)))
          (aig-ite (car x) zero one)))))

Theorem: aig-onehot-aux-zero-correct

(defthm aig-onehot-aux-zero-correct
  (b* (((mv acl2::?zero ?one)
        (aig-onehot-aux x)))
    (equal (aig-eval zero env)
           (equal (logcount (aig-list->u x env))
                  0))))

Theorem: aig-onehot-aux-one-correct

(defthm aig-onehot-aux-one-correct
  (b* (((mv acl2::?zero ?one)
        (aig-onehot-aux x)))
    (equal (aig-eval one env)
           (equal (logcount (aig-list->u x env))
                  1))))

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

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

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

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