		Search-engine friendly clone of the ACL2 documentation.

List-in

List-in-basics

Basic theorems about list-in, generated by std::deflist.

Definitions and Theorems

Theorem: list-in-of-cons

(defthm list-in-of-cons
  (equal (list-in (cons a x) set)
         (and (in a set) (list-in x set)))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-cdr-when-list-in

(defthm list-in-of-cdr-when-list-in
  (implies (list-in (double-rewrite x) set)
           (list-in (cdr x) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-when-not-consp

(defthm list-in-when-not-consp
  (implies (not (consp x))
           (list-in x set))
  :rule-classes ((:rewrite)))

Theorem: in-of-car-when-list-in

(defthm in-of-car-when-list-in
  (implies (list-in x set)
           (iff (in (car x) set)
                (or (consp x) (in nil set))))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-append

(defthm list-in-of-append
  (equal (list-in (append a b) set)
         (and (list-in a set) (list-in b set)))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-list-fix

(defthm list-in-of-list-fix
  (equal (list-in (acl2::list-fix x) set)
         (list-in x set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-sfix

(defthm list-in-of-sfix
  (iff (list-in (sfix x) set)
       (or (list-in x set) (not (setp x))))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-insert

(defthm list-in-of-insert
  (iff (list-in (insert a x) set)
       (and (list-in (sfix x) set) (in a set)))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-delete

(defthm list-in-of-delete
  (implies (list-in x set)
           (list-in (delete k x) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-mergesort

(defthm list-in-of-mergesort
  (iff (list-in (mergesort x) set)
       (list-in (acl2::list-fix x) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-union

(defthm list-in-of-union
  (iff (list-in (union x y) set)
       (and (list-in (sfix x) set)
            (list-in (sfix y) set)))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-intersect-1

(defthm list-in-of-intersect-1
  (implies (list-in x set)
           (list-in (intersect x y) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-intersect-2

(defthm list-in-of-intersect-2
  (implies (list-in y set)
           (list-in (intersect x y) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-difference

(defthm list-in-of-difference
  (implies (list-in x set)
           (list-in (difference x y) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-duplicated-members

(defthm list-in-of-duplicated-members
  (implies (list-in x set)
           (list-in (acl2::duplicated-members x)
                    set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-rev

(defthm list-in-of-rev
  (equal (list-in (acl2::rev x) set)
         (list-in (acl2::list-fix x) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-rcons

(defthm list-in-of-rcons
  (iff (list-in (acl2::rcons a x) set)
       (and (in a set)
            (list-in (acl2::list-fix x) set)))
  :rule-classes ((:rewrite)))

Theorem: in-when-member-equal-of-list-in

(defthm in-when-member-equal-of-list-in
  (and (implies (and (member-equal a x) (list-in x set))
                (in a set))
       (implies (and (list-in x set) (member-equal a x))
                (in a set)))
  :rule-classes ((:rewrite)))

Theorem: list-in-when-subsetp-equal

(defthm list-in-when-subsetp-equal
  (and (implies (and (subsetp-equal x y)
                     (list-in y set))
                (list-in x set))
       (implies (and (list-in y set)
                     (subsetp-equal x y))
                (list-in x set)))
  :rule-classes ((:rewrite)))

Theorem: list-in-set-equiv-congruence

(defthm list-in-set-equiv-congruence
  (implies (acl2::set-equiv x y)
           (equal (list-in x set) (list-in y set)))
  :rule-classes :congruence)

Theorem: list-in-of-set-difference-equal

(defthm list-in-of-set-difference-equal
  (implies (list-in x set)
           (list-in (set-difference-equal x y)
                    set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-intersection-equal-1

(defthm list-in-of-intersection-equal-1
  (implies (list-in (double-rewrite x) set)
           (list-in (intersection-equal x y) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-intersection-equal-2

(defthm list-in-of-intersection-equal-2
  (implies (list-in (double-rewrite y) set)
           (list-in (intersection-equal x y) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-union-equal

(defthm list-in-of-union-equal
  (equal (list-in (union-equal x y) set)
         (and (list-in (acl2::list-fix x) set)
              (list-in (double-rewrite y) set)))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-take

(defthm list-in-of-take
  (implies (list-in (double-rewrite x) set)
           (iff (list-in (take n x) set)
                (or (in nil set)
                    (<= (nfix n) (len x)))))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-repeat

(defthm list-in-of-repeat
  (iff (list-in (acl2::repeat n x) set)
       (or (in x set) (zp n)))
  :rule-classes ((:rewrite)))

Theorem: in-of-nth-when-list-in

(defthm in-of-nth-when-list-in
  (implies (and (list-in x set)
                (< (nfix n) (len x)))
           (in (nth n x) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-update-nth

(defthm list-in-of-update-nth
  (implies (list-in (double-rewrite x) set)
           (iff (list-in (update-nth n y x) set)
                (and (in y set)
                     (or (<= (nfix n) (len x))
                         (in nil set)))))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-butlast

(defthm list-in-of-butlast
  (implies (list-in (double-rewrite x) set)
           (list-in (butlast x n) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-nthcdr

(defthm list-in-of-nthcdr
  (implies (list-in (double-rewrite x) set)
           (list-in (nthcdr n x) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-last

(defthm list-in-of-last
  (implies (list-in (double-rewrite x) set)
           (list-in (last x) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-remove

(defthm list-in-of-remove
  (implies (list-in x set)
           (list-in (remove a x) set))
  :rule-classes ((:rewrite)))

Theorem: list-in-of-revappend

(defthm list-in-of-revappend
  (equal (list-in (revappend x y) set)
         (and (list-in (acl2::list-fix x) set)
              (list-in y set)))
  :rule-classes ((:rewrite)))