no-duplicates

(in-package "ACL2")

(defthm associativity-of-append
  (equal (append (append a b) c) (append a (append b c))))

(defthm member-equal-append
  (iff (member-equal x (append a b))
    (or (member-equal x a) (member-equal x b))))

(defthm no-duplicatesp-equal-append-iff
  (iff (no-duplicatesp-equal (append a b))
    (and (no-duplicatesp-equal a)
      (no-duplicatesp-equal b)
      (not (intersectp-equal (double-rewrite a) (double-rewrite b))))))

(defthm intersectp-equal-append1
  (equal (intersectp-equal (append a b) c)
    (or (intersectp-equal a c) (intersectp-equal b c))))

(defthm intersectp-equal-cons-second
  (iff (intersectp-equal a (cons c b))
    (or (member-equal c a) (intersectp-equal a b))))

(defthm intersectp-equal-non-cons-1
  (implies (not (consp a)) (not (intersectp-equal a b))))

(defthm intersectp-equal-non-cons
  (implies (not (consp b)) (not (intersectp-equal a b))))

(defthm intersectp-equal-append2
  (equal (intersectp-equal c (append a b))
    (or (intersectp-equal c a) (intersectp-equal c b))))

(defthm intersectp-equal-commute
  (iff (intersectp-equal a b) (intersectp-equal b a)))

(defthm no-duplicatesp-equal-non-cons
  (implies (not (consp x)) (no-duplicatesp-equal x)))