Some lemmas about 4vec-xfree-p in the
Theorem:
(defthm 4vec-<<=-when-xfree (implies (4vec-xfree-p x) (equal (4vec-<<= x y) (4vec-equiv x y))))
Theorem:
(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:
(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)))))