		Search-engine friendly clone of the ACL2 documentation.

Onehot-rewriting

4v-onehot-rw-sexpr

Apply onehot-rewriting to a single s-expression.

(4v-onehot-rw-sexpr vars sexpr) is given:

vars, which must be a nil-free list of atoms, and
sexpr, the s-expression we want to reduce.

It returns a new sexpression that is a (possibly simpler) conservative approximation of sexpr where the vars are assumed to be one-hot.

We usually don't call this function in practice, because 4v-onehot-rw-sexpr-alist uses a more efficient scheme that bypasses it. On the other hand, it's a nice function for reasoning about.

Definitions and Theorems

Function: 4v-onehot-rw-sexpr

(defun 4v-onehot-rw-sexpr (vars sexpr)
  (declare (xargs :guard (and (atom-listp vars)
                              (not (member-equal nil vars)))))
  (4vs-ite*-dumb (4vs-onehot vars)
                 (4v-onehot-sexpr-prime vars sexpr)
                 (4vs-x)))

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

(defthm 4v-sexpr-eval-of-4v-onehot-rw-sexpr
  (implies (and (atom-listp vars)
                (not (member-equal nil vars)))
           (4v-<= (4v-sexpr-eval (4v-onehot-rw-sexpr vars sexpr)
                                 env)
                  (4v-sexpr-eval sexpr env))))

Theorem: 4v-sexpr-<=-of-4v-onehot-rw-sexpr

(defthm 4v-sexpr-<=-of-4v-onehot-rw-sexpr
  (implies (and (atom-listp vars)
                (not (member-equal nil vars)))
           (4v-sexpr-<= (4v-onehot-rw-sexpr vars sexpr)
                        sexpr)))

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

(defthm 4v-sexpr-vars-of-4v-onehot-rw-sexpr
 (implies
      (atom-listp vars)
      (subsetp-equal (4v-sexpr-vars (4v-onehot-rw-sexpr vars sexpr))
                     (append vars (4v-sexpr-vars sexpr)))))