		Search-engine friendly clone of the ACL2 documentation.

4vec-xfree-p

4vec-xfree-p-basics

Some lemmas about 4vec-xfree-p in the sv/svex/lattice.lisp book.

Definitions and Theorems

Theorem: 4vec-<<=-when-xfree

(defthm 4vec-<<=-when-xfree
  (implies (4vec-xfree-p x)
           (equal (4vec-<<= x y)
                  (4vec-equiv x y))))

Theorem: svex-eval-when-4vec-xfree-of-minval

(defthm svex-eval-when-4vec-xfree-of-minval
  (implies (and (syntaxp (not (equal env ''nil)))
                (4vec-xfree-p (svex-xeval n)))
           (equal (svex-eval n env)
                  (svex-xeval n))))

Theorem: svex-eval-when-4vec-xfree-of-minval-apply

(defthm svex-eval-when-4vec-xfree-of-minval-apply
 (implies (and (syntaxp (not (equal env ''nil)))
               (not (eq (fnsym-fix fn) '===))
               (or (not (eq (fnsym-fix fn) '===*))
                   (svex-case (nth 1 args) :quote))
               (or (not (eq (fnsym-fix fn) '==?))
                   (svex-case (nth 1 args) :quote))
               (or (not (eq (fnsym-fix fn) 'bit?!))
                   (svex-case (nth 0 args) :quote))
               (or (not (eq (fnsym-fix fn) '?!))
                   (svex-case (nth 0 args) :quote))
               (4vec-xfree-p (svex-apply fn (svexlist-xeval args))))
          (equal (svex-apply fn (svexlist-eval args env))
                 (svex-apply fn (svexlist-xeval args)))))