• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
        • Rewriting
        • Svex
        • Bit-blasting
        • Functions
        • 4vmask
        • Why-infinite-width
        • Svex-vars
        • Evaluation
        • Values
          • 4vec
          • 4vec-<<=
            • 4vec-monotonicity
            • Svex-monotonify
            • Svex-alist-partial-monotonic
            • Svex-alist-monotonic-on-vars
            • 4veclist-<<=
            • Svexlist-partial-monotonic
            • Svex-partial-monotonic
            • Svex-alist-<<=
            • Svex-alist-ovmonotonic
            • Svexlist-<<=
            • Svex-env-<<=
            • Svex-alist-ovcongruent
            • Svex-alist-monotonic-p
            • Svexlist-monotonic-on-vars
            • Svex-monotonic-on-vars
            • Svex-<<=
            • Svexlist-monotonic-p
            • 4vec-xfree-p
            • Svex-apply-monotonocity
            • Svexlist-ovmonotonic
            • Svexlist-ovcongruent
            • Svex-ovmonotonic
            • Svex-monotonic-p
          • 3vec
          • 2vec
          • 2vecx
          • 2vecnatx
          • 4vec-x
          • 4vec-1x
          • 4vec-1z
          • 4vec-z
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• 4vec-<<=

Svex-alist-monotonic-on-vars

Definitions and Theorems

Theorem: svex-alist-monotonic-on-vars-necc

(defthm svex-alist-monotonic-on-vars-necc
  (implies (svex-alist-monotonic-on-vars vars x)
           (implies (and (svex-env-<<= env1 env2)
                         (svex-envs-agree-except vars env1 env2))
                    (svex-env-<<= (svex-alist-eval x env1)
                                  (svex-alist-eval x env2)))))

Theorem: svex-alist-monotonic-on-vars-of-svarlist-fix-vars

(defthm svex-alist-monotonic-on-vars-of-svarlist-fix-vars
  (equal (svex-alist-monotonic-on-vars (svarlist-fix vars)
                                       x)
         (svex-alist-monotonic-on-vars vars x)))

Theorem: svex-alist-monotonic-on-vars-svarlist-equiv-congruence-on-vars

(defthm
     svex-alist-monotonic-on-vars-svarlist-equiv-congruence-on-vars
  (implies (svarlist-equiv vars vars-equiv)
           (equal (svex-alist-monotonic-on-vars vars x)
                  (svex-alist-monotonic-on-vars vars-equiv x)))
  :rule-classes :congruence)

Theorem: set-equiv-implies-equal-svex-alist-monotonic-on-vars-1

(defthm set-equiv-implies-equal-svex-alist-monotonic-on-vars-1
  (implies (set-equiv vars vars-equiv)
           (equal (svex-alist-monotonic-on-vars vars x)
                  (svex-alist-monotonic-on-vars vars-equiv x)))
  :rule-classes (:congruence))

Theorem: svex-alist-eval-equiv-implies-equal-svex-alist-monotonic-on-vars-2

(defthm
 svex-alist-eval-equiv-implies-equal-svex-alist-monotonic-on-vars-2
 (implies (svex-alist-eval-equiv x x-equiv)
          (equal (svex-alist-monotonic-on-vars vars x)
                 (svex-alist-monotonic-on-vars vars x-equiv)))
 :rule-classes (:congruence))

Theorem: lookup-when-svex-alist-monotonic-on-vars

(defthm lookup-when-svex-alist-monotonic-on-vars
  (implies (svex-alist-monotonic-on-vars vars x)
           (svex-monotonic-on-vars vars (svex-lookup k x))))

Theorem: svex-compose-lookup-when-svex-alist-monotonic-on-vars

(defthm svex-compose-lookup-when-svex-alist-monotonic-on-vars
  (implies (svex-alist-monotonic-on-vars vars x)
           (svex-monotonic-on-vars vars (svex-compose-lookup k x))))

Theorem: svex-compose-preserves-svex-monotonic-on-vars

(defthm svex-compose-preserves-svex-monotonic-on-vars
  (implies (and (svex-monotonic-on-vars vars x)
                (svex-alist-monotonic-on-vars vars a)
                (subsetp-equal (svex-alist-keys a)
                               (svarlist-fix vars)))
           (svex-monotonic-on-vars vars (svex-compose x a))))

Theorem: svexlist-compose-preserves-svexlist-monotonic-on-vars

(defthm svexlist-compose-preserves-svexlist-monotonic-on-vars
 (implies (and (svexlist-monotonic-on-vars vars x)
               (svex-alist-monotonic-on-vars vars a)
               (subsetp-equal (svex-alist-keys a)
                              (svarlist-fix vars)))
          (svexlist-monotonic-on-vars vars (svexlist-compose x a))))

Theorem: svex-alist-compose-preserves-svex-alist-monotonic-on-vars

(defthm svex-alist-compose-preserves-svex-alist-monotonic-on-vars
 (implies
      (and (svex-alist-monotonic-on-vars vars x)
           (svex-alist-monotonic-on-vars vars a)
           (subsetp-equal (svex-alist-keys a)
                          (svarlist-fix vars)))
      (svex-alist-monotonic-on-vars vars (svex-alist-compose x a))))