		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-and-dumb

(4vs-and-dumb a b) constructs exactly the 4v-sexpr (and a b).

This is dumb in that it doesn't do the simple optimizations of 4vs-and, but it has a nicer 4v-sexpr-vars theorem because of this.

Definitions and Theorems

Function: 4vs-and-dumb

(defun 4vs-and-dumb (a b)
  (declare (xargs :guard t))
  (hons-list 'and a b))

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

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

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

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