		Search-engine friendly clone of the ACL2 documentation.

4vec-<<=

Svex-partial-monotonic

Definitions and Theorems

Theorem: svex-partial-monotonic-necc

(defthm svex-partial-monotonic-necc
  (implies (svex-partial-monotonic param-keys x)
           (implies (and (svex-alist-constantp setting)
                         (subsetp (svarlist-fix param-keys)
                                  (svex-alist-keys setting)))
                    (svex-monotonic-p (svex-compose x setting)))))

Theorem: eval-when-svex-partial-monotonic

(defthm eval-when-svex-partial-monotonic
  (implies (and (svex-partial-monotonic param-keys x)
                (equal (svex-env-extract param-keys env1)
                       (svex-env-extract param-keys env2))
                (svex-env-<<= env1 env2))
           (4vec-<<= (svex-eval x env1)
                     (svex-eval x env2))))

Function: svex-partial-monotonic-eval-witness

(defun svex-partial-monotonic-eval-witness (param-keys x)
  (b* ((setting (svex-partial-monotonic-witness param-keys x))
       (compose (svex-compose x setting))
       ((mv env1 env2)
        (svex-monotonic-p-witness compose))
       (setting-ev (svex-alist-eval setting nil)))
    (mv (append setting-ev env1)
        (append setting-ev env2))))

Theorem: svex-partial-monotonic-by-eval

(defthm svex-partial-monotonic-by-eval
  (equal (svex-partial-monotonic param-keys x)
         (b* (((mv env1 env2)
               (svex-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))
               (4vec-<<= (svex-eval x env1)
                         (svex-eval x env2)))))
  :rule-classes ((:definition :install-body nil)))

Theorem: svex-partial-monotonic-of-svarlist-fix-param-keys

(defthm svex-partial-monotonic-of-svarlist-fix-param-keys
  (equal (svex-partial-monotonic (svarlist-fix param-keys)
                                 x)
         (svex-partial-monotonic param-keys x)))

Theorem: svex-partial-monotonic-svarlist-equiv-congruence-on-param-keys

(defthm
     svex-partial-monotonic-svarlist-equiv-congruence-on-param-keys
  (implies (svarlist-equiv param-keys param-keys-equiv)
           (equal (svex-partial-monotonic param-keys x)
                  (svex-partial-monotonic param-keys-equiv x)))
  :rule-classes :congruence)

Theorem: set-equiv-implies-equal-svex-partial-monotonic-1

(defthm set-equiv-implies-equal-svex-partial-monotonic-1
  (implies (set-equiv param-keys param-keys-equiv)
           (equal (svex-partial-monotonic param-keys x)
                  (svex-partial-monotonic param-keys-equiv x)))
  :rule-classes (:congruence))

Theorem: svex-eval-equiv-implies-equal-svex-partial-monotonic-2

(defthm svex-eval-equiv-implies-equal-svex-partial-monotonic-2
  (implies (svex-eval-equiv x x-equiv)
           (equal (svex-partial-monotonic param-keys x)
                  (svex-partial-monotonic param-keys x-equiv)))
  :rule-classes (:congruence))