		Search-engine friendly clone of the ACL2 documentation.

4vec-<<=

Svex-alist-monotonic-p

Definitions and Theorems

Theorem: svex-alist-monotonic-p-necc

(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: svex-alist-eval-equiv-implies-equal-svex-alist-monotonic-p-1

(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: svex-monotonic-p-of-svex-lookup-when-svex-alist-monotonic-p

(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: svex-monotonic-p-of-svex-compose-lookup-when-svex-alist-monotonic-p

(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: svex-alist-monotonic-lookup-witness

(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: svex-alist-monotonic-in-terms-of-lookup

(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)))