• 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-<<=

Definitions and Theorems

Theorem: svex-alist-<<=-necc

(defthm svex-alist-<<=-necc
  (implies (svex-alist-<<= x y)
           (svex-env-<<= (svex-alist-eval x env)
                         (svex-alist-eval y env))))

Theorem: svex-alist-eval-equiv-implies-equal-svex-alist-<<=-1

(defthm svex-alist-eval-equiv-implies-equal-svex-alist-<<=-1
  (implies (svex-alist-eval-equiv x x-equiv)
           (equal (svex-alist-<<= x y)
                  (svex-alist-<<= x-equiv y)))
  :rule-classes (:congruence))

Theorem: svex-alist-eval-equiv-implies-equal-svex-alist-<<=-2

(defthm svex-alist-eval-equiv-implies-equal-svex-alist-<<=-2
  (implies (svex-alist-eval-equiv y y-equiv)
           (equal (svex-alist-<<= x y)
                  (svex-alist-<<= x y-equiv)))
  :rule-classes (:congruence))

Theorem: svex-<<=-of-svex-lookup-when-svex-alist-<<=

(defthm svex-<<=-of-svex-lookup-when-svex-alist-<<=
  (implies (svex-alist-<<= x y)
           (svex-<<= (svex-lookup k x)
                     (svex-lookup k y))))

Theorem: svex-<<=-of-svex-compose-lookup-when-svex-alist-<<=

(defthm svex-<<=-of-svex-compose-lookup-when-svex-alist-<<=
  (implies (and (svex-alist-<<= x y)
                (set-equiv (svex-alist-keys x)
                           (svex-alist-keys y)))
           (svex-<<= (svex-compose-lookup k x)
                     (svex-compose-lookup k y))))

Function: svex-alist-<<=-lookup-witness

(defun svex-alist-<<=-lookup-witness (x y)
  (svex-env-<<=-witness
       (svex-alist-eval x (svex-alist-<<=-witness x y))
       (svex-alist-eval y (svex-alist-<<=-witness x y))))

Theorem: svex-alist-<<=-in-terms-of-lookup

(defthm svex-alist-<<=-in-terms-of-lookup
  (equal (svex-alist-<<= x y)
         (let ((var (svex-alist-<<=-lookup-witness x y)))
           (svex-<<= (svex-lookup var x)
                     (svex-lookup var y))))
  :rule-classes ((:definition :install-body nil)))

Theorem: svex-alist-<<=-refl

(defthm svex-alist-<<=-refl
  (svex-alist-<<= x x))

Theorem: svex-alist-<<=-transitive-1

(defthm svex-alist-<<=-transitive-1
  (implies (and (svex-alist-<<= x y)
                (svex-alist-<<= y z))
           (svex-alist-<<= x z)))

Theorem: svex-alist-<<=-transitive-2

(defthm svex-alist-<<=-transitive-2
  (implies (and (svex-alist-<<= y z)
                (svex-alist-<<= x y))
           (svex-alist-<<= x z)))

Theorem: svex-alist-<<=-asymm

(defthm svex-alist-<<=-asymm
  (implies (and (svex-alist-<<= x y)
                (set-equiv (svex-alist-keys x)
                           (svex-alist-keys y)))
           (iff (svex-alist-<<= y x)
                (svex-alist-eval-equiv y x))))