		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-xor

(4vs-xor a b) constructs a sexpr representing (xor a b).

Definitions and Theorems

Function: 4vs-xor

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

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

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