		Search-engine friendly clone of the ACL2 documentation.

4v-onehot-list-p

(4v-onehot-list-p x) determines if a list of 4vps has exactly one member that is T while the rest are F.

Definitions and Theorems

Function: 4v-onehot-list-p

(defun 4v-onehot-list-p (x)
  (declare (xargs :guard t))
  (if (atom x)
      nil
    (4vcases (car x)
             (f (4v-onehot-list-p (cdr x)))
             (t (all-equalp *4vf* (cdr x)))
             (& nil))))

Theorem: 4v-onehot-list-p-when-atom

(defthm 4v-onehot-list-p-when-atom
  (implies (atom x)
           (equal (4v-onehot-list-p x) nil)))

Theorem: 4v-onehot-list-p-of-cons

(defthm 4v-onehot-list-p-of-cons
  (equal (4v-onehot-list-p (cons a x))
         (4vcases a (f (4v-onehot-list-p x))
                  (t (all-equalp *4vf* x))
                  (& nil))))