		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-zif-dumb

(4vs-zif-dumb c a b) constructs (ZIF C A B), i.e., the s-expression for an pass-gate style multiplexor.

Definitions and Theorems

Function: 4vs-zif-dumb$inline

(defun 4vs-zif-dumb$inline (c a b)
  (declare (xargs :guard t))
  (hons-list 'zif c a b))

Theorem: 4v-sexpr-eval-of-4vs-zif-dumb

(defthm 4v-sexpr-eval-of-4vs-zif-dumb
  (equal (4v-sexpr-eval (4vs-zif-dumb c a b) env)
         (4v-zif (4v-sexpr-eval c env)
                 (4v-sexpr-eval a env)
                 (4v-sexpr-eval b env))))

Theorem: 4v-sexpr-vars-of-4vs-zif-dumb

(defthm 4v-sexpr-vars-of-4vs-zif-dumb
 (equal
   (4v-sexpr-vars (4vs-zif-dumb c a b))
   (hons-alphorder-merge (4v-sexpr-vars c)
                         (hons-alphorder-merge (4v-sexpr-vars a)
                                               (4v-sexpr-vars b)))))