		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-or

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

Definitions and Theorems

Function: 4vs-or

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

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

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