Theorem:
(defthm svex-mono-eval-monotonic (implies (svex-env-<<= env1 env2) (4vec-<<= (svex-mono-eval x env1) (svex-mono-eval x env2))))
Theorem:
(defthm svex-call-mono-eval-monotonic (implies (svex-env-<<= env1 env2) (4vec-<<= (svex-call-mono-eval x env1) (svex-call-mono-eval x env2))))
Theorem:
(defthm svex-fn/args-mono-eval-monotonic (implies (svex-env-<<= env1 env2) (4vec-<<= (svex-fn/args-mono-eval fn args env1) (svex-fn/args-mono-eval fn args env2))))
Theorem:
(defthm svexlist-mono-eval-monotonic (implies (svex-env-<<= env1 env2) (4veclist-<<= (svexlist-mono-eval x env1) (svexlist-mono-eval x env2))))
Theorem:
(defthm svex-alist-mono-eval-monotonic (implies (svex-env-<<= env1 env2) (svex-env-<<= (svex-alist-mono-eval x env1) (svex-alist-mono-eval x env2))))
Theorem:
(defthm svex-eval-gte-mono-eval (4vec-<<= (svex-mono-eval x env) (svex-eval x env)))
Theorem:
(defthm svexlist-eval-gte-mono-eval (4veclist-<<= (svexlist-mono-eval x env) (svexlist-eval x env)))
Theorem:
(defthm svex-alist-eval-gte-mono-eval (svex-env-<<= (svex-alist-mono-eval x env) (svex-alist-eval x env)))
Theorem:
(defthm svex-eval-gte-xeval (4vec-<<= (svex-xeval x) (svex-eval x env)))
Theorem:
(defthm svexlist-eval-gte-xeval (4veclist-<<= (svexlist-xeval x) (svexlist-eval x env)))
Theorem:
(defthm svex-alist-eval-gte-xeval (svex-env-<<= (svex-alist-xeval x) (svex-alist-eval x env)))
Accordingly, we can often use svex-mono-eval in place of svex-eval.
Theorem:
(defthm svex-eval-when-2vec-p-of-minval (implies (and (syntaxp (not (equal env ''nil))) (2vec-p (svex-mono-eval n env))) (equal (svex-eval n env) (svex-mono-eval n env))))
Theorem:
(defthm logbitp-when-4vec-<<=-svex-eval-strong (implies (syntaxp (not (equal env ''nil))) (and (equal (logbitp n (4vec->upper (svex-eval b env))) (if (bit->bool (b-ior (b-not (logbit n (4vec->upper (svex-xeval b)))) (logbit n (4vec->lower (svex-xeval b))))) (logbitp n (4vec->upper (svex-xeval b))) (bit-n n (4vec->upper (svex-eval b env))))) (equal (logbitp n (4vec->lower (svex-eval b env))) (if (bit->bool (b-ior (b-not (logbit n (4vec->upper (svex-xeval b)))) (logbit n (4vec->lower (svex-xeval b))))) (logbitp n (4vec->lower (svex-xeval b))) (bit-n n (4vec->lower (svex-eval b env))))))))