Theorem:
(defthm svexlist-partial-monotonic-necc (implies (svexlist-partial-monotonic param-keys x) (implies (and (svex-alist-constantp setting) (subsetp (svarlist-fix param-keys) (svex-alist-keys setting))) (svexlist-monotonic-p (svexlist-compose x setting)))))
Theorem:
(defthm eval-when-svexlist-partial-monotonic (implies (and (svexlist-partial-monotonic param-keys x) (equal (svex-env-extract param-keys env1) (svex-env-extract param-keys env2)) (svex-env-<<= env1 env2)) (4veclist-<<= (svexlist-eval x env1) (svexlist-eval x env2))))
Function:
(defun svexlist-partial-monotonic-eval-witness (param-keys x) (b* ((setting (svexlist-partial-monotonic-witness param-keys x)) (compose (svexlist-compose x setting)) ((mv env1 env2) (svexlist-monotonic-p-witness compose)) (setting-ev (svex-alist-eval setting nil))) (mv (append setting-ev env1) (append setting-ev env2))))
Theorem:
(defthm svexlist-partial-monotonic-by-eval (equal (svexlist-partial-monotonic param-keys x) (b* (((mv env1 env2) (svexlist-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)) (4veclist-<<= (svexlist-eval x env1) (svexlist-eval x env2))))) :rule-classes ((:definition :install-body nil)))
Theorem:
(defthm svexlist-partial-monotonic-of-svarlist-fix-param-keys (equal (svexlist-partial-monotonic (svarlist-fix param-keys) x) (svexlist-partial-monotonic param-keys x)))
Theorem:
(defthm svexlist-partial-monotonic-svarlist-equiv-congruence-on-param-keys (implies (svarlist-equiv param-keys param-keys-equiv) (equal (svexlist-partial-monotonic param-keys x) (svexlist-partial-monotonic param-keys-equiv x))) :rule-classes :congruence)
Theorem:
(defthm set-equiv-implies-equal-svexlist-partial-monotonic-1 (implies (set-equiv param-keys param-keys-equiv) (equal (svexlist-partial-monotonic param-keys x) (svexlist-partial-monotonic param-keys-equiv x))) :rule-classes (:congruence))
Theorem:
(defthm svexlist-eval-equiv-implies-svexlist-eval-equiv-svexlist-compose-1 (implies (svexlist-eval-equiv x x-equiv) (svexlist-eval-equiv (svexlist-compose x a) (svexlist-compose x-equiv a))) :rule-classes (:congruence))
Theorem:
(defthm svexlist-eval-equiv-implies-equal-svexlist-partial-monotonic-2 (implies (svexlist-eval-equiv x x-equiv) (equal (svexlist-partial-monotonic param-keys x) (svexlist-partial-monotonic param-keys x-equiv))) :rule-classes (:congruence))