(4v-onehot-list-p x) determines if a list of 4vps has
exactly one member that is
Function:
(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:
(defthm 4v-onehot-list-p-when-atom (implies (atom x) (equal (4v-onehot-list-p x) nil)))
Theorem:
(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))))