		Search-engine friendly clone of the ACL2 documentation.

4vs-constructors

4vs-not

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

Definitions and Theorems

Function: 4vs-not

(defun 4vs-not (a)
  (declare (xargs :guard t))
  (b* (((when (atom a)) (hons-list 'not a))
       (fn (car a))
       (args (cdr a)))
    (case fn
      ((t)
       (if (not args)
           *4vf-sexpr*
         (hons-list 'not a)))
      ((f)
       (if (not args)
           *4vt-sexpr*
         (hons-list 'not a)))
      ((x z)
       (if (not args)
           *4vx-sexpr*
         (hons-list 'not a)))
      (not (if (and (consp args) (not (cdr args)))
               (4vs-buf (first args))
             (hons-list 'not a)))
      (buf (if (and (consp args) (not (cdr args)))
               (hons-list 'not (first args))
             (hons-list 'not a)))
      (otherwise (hons-list 'not a)))))

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

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

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

(defthm 4v-sexpr-vars-of-4vs-not
  (equal (4v-sexpr-vars (4vs-not a))
         (4v-sexpr-vars a)))