Theorem:
(defthm svex-alist-monotonic-p-necc (implies (svex-alist-monotonic-p x) (implies (svex-env-<<= env1 env2) (svex-env-<<= (svex-alist-eval x env1) (svex-alist-eval x env2)))))
Theorem:
(defthm svex-alist-eval-equiv-implies-equal-svex-alist-monotonic-p-1 (implies (svex-alist-eval-equiv x x-equiv) (equal (svex-alist-monotonic-p x) (svex-alist-monotonic-p x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm svex-monotonic-p-of-svex-lookup-when-svex-alist-monotonic-p (implies (svex-alist-monotonic-p x) (svex-monotonic-p (svex-lookup k x))))
Theorem:
(defthm svex-monotonic-p-of-svex-compose-lookup-when-svex-alist-monotonic-p (implies (svex-alist-monotonic-p x) (svex-monotonic-p (svex-compose-lookup k x))))
Function:
(defun svex-alist-monotonic-lookup-witness (x) (mv-let (env1 env2) (svex-alist-monotonic-p-witness x) (svex-env-<<=-witness (svex-alist-eval x env1) (svex-alist-eval x env2))))
Theorem:
(defthm svex-alist-monotonic-in-terms-of-lookup (equal (svex-alist-monotonic-p x) (let ((var (svex-alist-monotonic-lookup-witness x))) (svex-monotonic-p (svex-lookup var x)))) :rule-classes ((:definition :install-body nil)))