Theorem:
(defthm svex-alist-partial-monotonic-necc (implies (svex-alist-partial-monotonic param-keys x) (implies (and (svex-alist-constantp setting) (subsetp (svarlist-fix param-keys) (svex-alist-keys setting))) (svex-alist-monotonic-p (svex-alist-compose x setting)))))
Theorem:
(defthm eval-when-svex-alist-partial-monotonic (implies (and (svex-alist-partial-monotonic param-keys x) (equal (svex-env-extract param-keys env1) (svex-env-extract param-keys env2)) (svex-env-<<= env1 env2)) (svex-env-<<= (svex-alist-eval x env1) (svex-alist-eval x env2))))
Function:
(defun svex-alist-partial-monotonic-eval-witness (param-keys x) (b* ((setting (svex-alist-partial-monotonic-witness param-keys x)) (compose (svex-alist-compose x setting)) ((mv env1 env2) (svex-alist-monotonic-p-witness compose)) (setting-ev (svex-alist-eval setting nil))) (mv (append setting-ev env1) (append setting-ev env2))))
Theorem:
(defthm svex-alist-partial-monotonic-by-eval (equal (svex-alist-partial-monotonic param-keys x) (b* (((mv env1 env2) (svex-alist-partial-monotonic-eval-witness param-keys x))) (or (not (equal (svex-env-extract param-keys env1) (svex-env-extract param-keys env2))) (not (svex-env-<<= env1 env2)) (svex-env-<<= (svex-alist-eval x env1) (svex-alist-eval x env2))))) :rule-classes ((:definition :install-body nil)))
Theorem:
(defthm lookup-when-svex-alist-partial-monotonic (implies (svex-alist-partial-monotonic param-keys x) (svex-partial-monotonic param-keys (svex-lookup k x))))
Theorem:
(defthm svex-compose-lookup-when-svex-alist-partial-monotonic (implies (svex-alist-partial-monotonic param-keys x) (svex-partial-monotonic param-keys (svex-compose-lookup k x))))
Theorem:
(defthm svex-alist-partial-monotonic-of-svarlist-fix-param-keys (equal (svex-alist-partial-monotonic (svarlist-fix param-keys) x) (svex-alist-partial-monotonic param-keys x)))
Theorem:
(defthm svex-alist-partial-monotonic-svarlist-equiv-congruence-on-param-keys (implies (svarlist-equiv param-keys param-keys-equiv) (equal (svex-alist-partial-monotonic param-keys x) (svex-alist-partial-monotonic param-keys-equiv x))) :rule-classes :congruence)
Theorem:
(defthm set-equiv-implies-equal-svex-alist-partial-monotonic-1 (implies (set-equiv param-keys param-keys-equiv) (equal (svex-alist-partial-monotonic param-keys x) (svex-alist-partial-monotonic param-keys-equiv x))) :rule-classes (:congruence))
Theorem:
(defthm svex-compose-preserves-svex-partial-monotonic (implies (and (svex-partial-monotonic params x) (svex-alist-partial-monotonic params2 a) (svex-compose-alist-const/selfbound-keys-p params a)) (svex-partial-monotonic (append params params2) (svex-compose x a))))
Theorem:
(defthm svex-alist-eval-equiv-implies-svexlist-eval-equiv-svexlist-compose-2 (implies (svex-alist-eval-equiv a a-equiv) (svexlist-eval-equiv (svexlist-compose x a) (svexlist-compose x a-equiv))) :rule-classes (:congruence))
Theorem:
(defthm svexlist-compose-preserves-svexlist-partial-monotonic (implies (and (svexlist-partial-monotonic params x) (svex-alist-partial-monotonic params2 a) (svex-compose-alist-const/selfbound-keys-p params a)) (svexlist-partial-monotonic (append params params2) (svexlist-compose x a))))
Theorem:
(defthm svex-alist-compose-preserves-svex-alist-partial-monotonic (implies (and (svex-alist-partial-monotonic params x) (svex-alist-partial-monotonic params2 a) (svex-compose-alist-const/selfbound-keys-p params a)) (svex-alist-partial-monotonic (append params params2) (svex-alist-compose x a))))
Theorem:
(defthm svex-alist-eval-equiv-implies-equal-svex-alist-partial-monotonic-2 (implies (svex-alist-eval-equiv x x-equiv) (equal (svex-alist-partial-monotonic param-keys x) (svex-alist-partial-monotonic param-keys x-equiv))) :rule-classes (:congruence))