		Search-engine friendly clone of the ACL2 documentation.

4vs-onehot

(4vs-onehot sexprs) constructs an s-expression that is T when the members of X are one-hot.

X should be a list of s-expressions, say (A1 ... AN). The s-expression we construct to check whether these are one-hot is somewhat ugly, and looks something like this:

(ITE* A1
      (AND (NOT A2) (NOT A3) ... (NOT AN))
  (ITE* A2
        (AND (NOT A3) ... (NOT AN))
    (ITE* AN
          (T)
        (F)) ...))

Note that although the printed representation is particularly large looking, the AND terms here can be mostly structure shared. For instance, the [~A2...~AN] term is really just (AND (NOT A2) [~A3...~AN]), so by honsing sexprs we get a lot of reuse here.

Definitions and Theorems

Function: 4vs-onehot

(defun 4vs-onehot (sexprs)
  (declare (xargs :guard t))
  (if (atom sexprs)
      (4vs-f)
    (4vs-ite*-dumb (car sexprs)
                   (4vs-and-list-dumb (4vs-not-list (cdr sexprs)))
                   (4vs-onehot (cdr sexprs)))))

Theorem: 4v-sexpr-eval-of-4vs-onehot

(defthm 4v-sexpr-eval-of-4vs-onehot
  (equal (equal (4v-sexpr-eval (4vs-onehot sexprs) env)
                *4vt*)
         (4v-onehot-list-p (4v-sexpr-eval-list sexprs env))))

Theorem: 4v-sexpr-vars-of-4vs-onehot

(defthm 4v-sexpr-vars-of-4vs-onehot
  (set-equiv (4v-sexpr-vars (4vs-onehot sexprs))
             (4v-sexpr-vars-list sexprs)))

Subtopics

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.