• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Listpos
      • List-equiv
        • Basic-list-equiv-congruences
        • List-equiv-reductions
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• List-equiv

Basic-list-equiv-congruences

Basic list-equiv congruence theorems for built-in functions.

Definitions and Theorems

Theorem: list-equiv-implies-equal-list-fix-1

(defthm list-equiv-implies-equal-list-fix-1
  (implies (list-equiv x x-equiv)
           (equal (list-fix x) (list-fix x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-car-1

(defthm list-equiv-implies-equal-car-1
  (implies (list-equiv x x-equiv)
           (equal (car x) (car x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-cdr-1

(defthm list-equiv-implies-list-equiv-cdr-1
  (implies (list-equiv x x-equiv)
           (list-equiv (cdr x) (cdr x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-cons-2

(defthm list-equiv-implies-list-equiv-cons-2
  (implies (list-equiv y y-equiv)
           (list-equiv (cons x y)
                       (cons x y-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-nth-2

(defthm list-equiv-implies-equal-nth-2
  (implies (list-equiv x x-equiv)
           (equal (nth n x) (nth n x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-nthcdr-2

(defthm list-equiv-implies-list-equiv-nthcdr-2
  (implies (list-equiv x x-equiv)
           (list-equiv (nthcdr n x)
                       (nthcdr n x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-update-nth-3

(defthm list-equiv-implies-list-equiv-update-nth-3
  (implies (list-equiv x x-equiv)
           (list-equiv (update-nth n v x)
                       (update-nth n v x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-consp-1

(defthm list-equiv-implies-equal-consp-1
  (implies (list-equiv x x-equiv)
           (equal (consp x) (consp x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-len-1

(defthm list-equiv-implies-equal-len-1
  (implies (list-equiv x x-equiv)
           (equal (len x) (len x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-append-1

(defthm list-equiv-implies-equal-append-1
  (implies (list-equiv x x-equiv)
           (equal (append x y) (append x-equiv y)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-append-2

(defthm list-equiv-implies-list-equiv-append-2
  (implies (list-equiv y y-equiv)
           (list-equiv (append x y)
                       (append x y-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-member-2

(defthm list-equiv-implies-list-equiv-member-2
  (implies (list-equiv x x-equiv)
           (list-equiv (member k x)
                       (member k x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-iff-member-2

(defthm list-equiv-implies-iff-member-2
  (implies (list-equiv x x-equiv)
           (iff (member k x) (member k x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-subsetp-1

(defthm list-equiv-implies-equal-subsetp-1
  (implies (list-equiv x x-equiv)
           (equal (subsetp x y)
                  (subsetp x-equiv y)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-subsetp-2

(defthm list-equiv-implies-equal-subsetp-2
  (implies (list-equiv y y-equiv)
           (equal (subsetp x y)
                  (subsetp x y-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-remove-2

(defthm list-equiv-implies-equal-remove-2
  (implies (list-equiv x x-equiv)
           (equal (remove a x) (remove a x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-resize-list-1

(defthm list-equiv-implies-equal-resize-list-1
  (implies (list-equiv lst lst-equiv)
           (equal (resize-list lst n default)
                  (resize-list lst-equiv n default)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-revappend-1

(defthm list-equiv-implies-equal-revappend-1
  (implies (list-equiv x x-equiv)
           (equal (revappend x y)
                  (revappend x-equiv y)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-revappend-2

(defthm list-equiv-implies-list-equiv-revappend-2
  (implies (list-equiv y y-equiv)
           (list-equiv (revappend x y)
                       (revappend x y-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-last-1

(defthm list-equiv-implies-list-equiv-last-1
  (implies (list-equiv x x-equiv)
           (list-equiv (last x) (last x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-make-list-ac-3

(defthm list-equiv-implies-list-equiv-make-list-ac-3
  (implies (list-equiv ac ac-equiv)
           (list-equiv (make-list-ac n val ac)
                       (make-list-ac n val ac-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-no-duplicatesp-equal-1

(defthm list-equiv-implies-equal-no-duplicatesp-equal-1
  (implies (list-equiv x x-equiv)
           (equal (no-duplicatesp-equal x)
                  (no-duplicatesp-equal x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-string-append-lst-1

(defthm list-equiv-implies-equal-string-append-lst-1
  (implies (list-equiv x x-equiv)
           (equal (string-append-lst x)
                  (string-append-lst x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-assoc-equal-2

(defthm list-equiv-implies-equal-assoc-equal-2
  (implies (list-equiv l l-equiv)
           (equal (assoc-equal x l)
                  (assoc-equal x l-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-strip-cars-1

(defthm list-equiv-implies-equal-strip-cars-1
  (implies (list-equiv x x-equiv)
           (equal (strip-cars x)
                  (strip-cars x-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-equal-remove-assoc-equal-2

(defthm list-equiv-implies-equal-remove-assoc-equal-2
  (implies (list-equiv l l-equiv)
           (equal (remove-assoc-equal x l)
                  (remove-assoc-equal x l-equiv)))
  :rule-classes (:congruence))

Theorem: list-equiv-implies-list-equiv-put-assoc-equal-3

(defthm list-equiv-implies-list-equiv-put-assoc-equal-3
  (implies (list-equiv alist alist-equiv)
           (list-equiv (put-assoc-equal name val alist)
                       (put-assoc-equal name val alist-equiv)))
  :rule-classes (:congruence))