		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-and

(4vs-and a b) constructs a 4v-sexpr equivalent to (and a b).

Definitions and Theorems

Function: 4vs-and

(defun 4vs-and (a b)
  (declare (xargs :guard t))
  (cond ((or (atom a) (atom b))
         (cond ((equal a b) (4vs-buf a))
               (t (hons-list 'and a b))))
        ((4vf-sexpr-p a) a)
        ((4vf-sexpr-p b) b)
        ((4vt-sexpr-p a) (4vs-buf b))
        ((4vt-sexpr-p b) (4vs-buf a))
        ((hons-equal a b) (4vs-buf a))
        (t (hons-list 'and a b))))

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

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

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

(defthm 4v-sexpr-vars-of-4vs-and
  (subsetp-equal (4v-sexpr-vars (4vs-and a b))
                 (append (4v-sexpr-vars a)
                         (4v-sexpr-vars b))))