		Search-engine friendly clone of the ACL2 documentation.

Sexpr-equivs

4v-sexpr-alist-pair-equiv

Element equivalence for sexpr alists.

This is a universal equivalence, introduced using def-universal-equiv.

Function: 4v-sexpr-alist-pair-equiv

(defun 4v-sexpr-alist-pair-equiv (x y)
  (and (iff (consp x) (consp y))
       (equal (car x) (car y))
       (4v-sexpr-equiv (cdr x) (cdr y))))

Definitions and Theorems

Function: 4v-sexpr-alist-pair-equiv

(defun 4v-sexpr-alist-pair-equiv (x y)
  (and (iff (consp x) (consp y))
       (equal (car x) (car y))
       (4v-sexpr-equiv (cdr x) (cdr y))))

Theorem: 4v-sexpr-alist-pair-equiv-is-an-equivalence

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

Theorem: 4v-sexpr-equiv-implies-4v-sexpr-alist-pair-equiv-cons-2

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

Theorem: 4v-sexpr-alist-pair-equiv-implies-4v-sexpr-equiv-cdr-1

(defthm 4v-sexpr-alist-pair-equiv-implies-4v-sexpr-equiv-cdr-1
  (implies (4v-sexpr-alist-pair-equiv x x-equiv)
           (4v-sexpr-equiv (cdr x) (cdr x-equiv)))
  :rule-classes (:congruence))