• Top
  • Documentation
  • Books
  • Boolean-reasoning
    • Ipasir
    • Aignet
    • Aig
    • Satlink
    • Truth
    • Ubdds
    • Bdd
    • Faig
    • Bed
    • 4v
      • 4v-sexprs
        • 4v-sexpr-vars
        • 4v-sexpr-eval
        • 4v-sexpr-to-faig
        • 4v-sexpr-restrict-with-rw
        • 4vs-constructors
        • 4v-sexpr-compose-with-rw
        • 4v-sexpr-restrict
        • 4v-sexpr-alist-extract
        • 4v-sexpr-compose
        • 4v-nsexpr-p
        • 4v-sexpr-purebool-p
        • 4v-sexpr-<=
        • Sfaig
        • Sexpr-equivs
          • 4v-sexpr-alist-equiv
          • 4v-env-equiv
          • 4v-sexpr-list-equiv
          • 4v-sexpr-equiv
          • 4v-alists-agree
          • Key-and-env-equiv
          • 4v-sexpr-alist-equiv-alt
          • 4v-sexpr-alist-pair-equiv
          • 4v-cdr-consp-equiv
          • 4v-cdr-equiv
        • 3v-syntax-sexprp
        • Sexpr-rewriting
        • 4v-sexpr-ind
        • 4v-alist-extract
      • 4v-monotonicity
      • 4v-operations
      • Why-4v-logic
      • 4v-<=
      • 4vp
      • 4vcases
      • 4v-fix
      • 4v-lookup
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Sexpr-equivs

4v-env-equiv

Equivalence of four-valued environments (alists).

X === Y in the sense of four-valued environments if X[k] === Y[k] for all keys k, in the sense of 4v-equiv.

Function: 4v-env-equiv

(defun 4v-env-equiv (x y)
  (declare (xargs :non-executable t))
  (declare (xargs :guard t))
  (declare (xargs :non-executable t))
  (prog2$ (throw-nonexec-error '4v-env-equiv
                               (list x y))
          (let ((key (4v-env-equiv-witness x y)))
            (and (equal (4v-lookup key x)
                        (4v-lookup key y))))))

Definitions and Theorems

Theorem: 4v-env-equiv-necc

(defthm 4v-env-equiv-necc
  (implies (not (and (equal (4v-lookup key x)
                            (4v-lookup key y))))
           (not (4v-env-equiv x y))))

Theorem: 4v-env-equiv-witnessing-witness-rule-correct

(defthm 4v-env-equiv-witnessing-witness-rule-correct
  (implies (not ((lambda (key y x)
                   (not (equal (4v-lookup key x)
                               (4v-lookup key y))))
                 (4v-env-equiv-witness x y)
                 y x))
           (4v-env-equiv x y))
  :rule-classes nil)

Theorem: 4v-env-equiv-instancing-instance-rule-correct

(defthm 4v-env-equiv-instancing-instance-rule-correct
  (implies (not (equal (4v-lookup key x)
                       (4v-lookup key y)))
           (not (4v-env-equiv x y)))
  :rule-classes nil)

Theorem: 4v-env-equiv-is-an-equivalence

(defthm 4v-env-equiv-is-an-equivalence
  (and (booleanp (4v-env-equiv x y))
       (4v-env-equiv x x)
       (implies (4v-env-equiv x y)
                (4v-env-equiv y x))
       (implies (and (4v-env-equiv x y)
                     (4v-env-equiv y z))
                (4v-env-equiv x z)))
  :rule-classes (:equivalence))

Theorem: alist-equiv-refines-4v-env-equiv

(defthm alist-equiv-refines-4v-env-equiv
  (implies (alist-equiv x y)
           (4v-env-equiv x y))
  :rule-classes (:refinement))

Theorem: 4v-env-equiv-implies-4v-env-equiv-cons-2

(defthm 4v-env-equiv-implies-4v-env-equiv-cons-2
  (implies (4v-env-equiv b b-equiv)
           (4v-env-equiv (cons a b)
                         (cons a b-equiv)))
  :rule-classes (:congruence))

Theorem: 4v-env-equiv-implies-4v-env-equiv-append-2

(defthm 4v-env-equiv-implies-4v-env-equiv-append-2
  (implies (4v-env-equiv b b-equiv)
           (4v-env-equiv (append a b)
                         (append a b-equiv)))
  :rule-classes (:congruence))

Theorem: 4v-env-equiv-implies-iff-4v-alist-<=-1

(defthm 4v-env-equiv-implies-iff-4v-alist-<=-1
  (implies (4v-env-equiv a a-equiv)
           (iff (4v-alist-<= a b)
                (4v-alist-<= a-equiv b)))
  :rule-classes (:congruence))

Theorem: 4v-env-equiv-implies-iff-4v-alist-<=-2

(defthm 4v-env-equiv-implies-iff-4v-alist-<=-2
  (implies (4v-env-equiv b b-equiv)
           (iff (4v-alist-<= a b)
                (4v-alist-<= a b-equiv)))
  :rule-classes (:congruence))

Theorem: 4v-env-equiv-implies-equal-4v-lookup-2

(defthm 4v-env-equiv-implies-equal-4v-lookup-2
  (implies (4v-env-equiv al al-equiv)
           (equal (4v-lookup k al)
                  (4v-lookup k al-equiv)))
  :rule-classes (:congruence))

Theorem: 4v-env-equiv-implies-4v-cdr-equiv-hons-assoc-equal-2

(defthm 4v-env-equiv-implies-4v-cdr-equiv-hons-assoc-equal-2
  (implies (4v-env-equiv y y-equiv)
           (4v-cdr-equiv (hons-assoc-equal x y)
                         (hons-assoc-equal x y-equiv)))
  :rule-classes (:congruence))

Theorem: 4v-cdr-consp-equiv-implies-4v-env-equiv-cons-1

(defthm 4v-cdr-consp-equiv-implies-4v-env-equiv-cons-1
  (implies (4v-cdr-consp-equiv a a-equiv)
           (4v-env-equiv (cons a b)
                         (cons a-equiv b)))
  :rule-classes (:congruence))

Theorem: 4v-env-equiv-implies-equal-4v-sexpr-eval-2

(defthm 4v-env-equiv-implies-equal-4v-sexpr-eval-2
  (implies (4v-env-equiv env1 env2)
           (equal (4v-sexpr-eval x env1)
                  (4v-sexpr-eval x env2)))
  :rule-classes :congruence)

Theorem: 4v-env-equiv-implies-equal-4v-sexpr-eval-list-2

(defthm 4v-env-equiv-implies-equal-4v-sexpr-eval-list-2
  (implies (4v-env-equiv env1 env2)
           (equal (4v-sexpr-eval-list x env1)
                  (4v-sexpr-eval-list x env2)))
  :rule-classes :congruence)

Theorem: 4v-env-equiv-implies-equal-4v-sexpr-eval-alist-2

(defthm 4v-env-equiv-implies-equal-4v-sexpr-eval-alist-2
  (implies (4v-env-equiv env env-equiv)
           (equal (4v-sexpr-eval-alist x env)
                  (4v-sexpr-eval-alist x env-equiv)))
  :rule-classes (:congruence))

Theorem: 4v-env-equiv-append

(defthm 4v-env-equiv-append
  (implies (and (set-equiv (double-rewrite (alist-keys a))
                           (double-rewrite (alist-keys b)))
                (4v-env-equiv (double-rewrite a)
                              (double-rewrite b))
                (4v-env-equiv (double-rewrite c)
                              (double-rewrite d)))
           (equal (4v-env-equiv (append a c) (append b d))
                  t)))