Filtering...

no-duplicatesp-equal

books/kestrel/lists-light/no-duplicatesp-equal

Included Books

member-equal intersection-equal
other
(in-package "ACL2")
local
(local (include-book "member-equal"))
local
(local (include-book "intersection-equal"))
in-theory
(in-theory (disable no-duplicatesp-equal))
no-duplicatesp-equal-when-not-consp-cheaptheorem
(defthm no-duplicatesp-equal-when-not-consp-cheap
  (implies (not (consp x)) (no-duplicatesp-equal x))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal))))
no-duplicatesp-equal-of-cdrtheorem
(defthm no-duplicatesp-equal-of-cdr
  (implies (no-duplicatesp-equal x)
    (no-duplicatesp-equal (cdr x)))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal))))
no-duplicatesp-equal-of-member-equaltheorem
(defthm no-duplicatesp-equal-of-member-equal
  (implies (no-duplicatesp-equal x)
    (no-duplicatesp-equal (member-equal a x)))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal member-equal))))
no-duplicatesp-equal-when-no-duplicatesp-equal-of-cdrtheorem
(defthm no-duplicatesp-equal-when-no-duplicatesp-equal-of-cdr
  (implies (and (no-duplicatesp-equal (cdr x))
      (not (member-equal (car x) (cdr x))))
    (no-duplicatesp-equal x))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal member-equal)
     :induct (no-duplicatesp-equal x))))
not-member-equal-of-cdr-of-member-equaltheorem
(defthm not-member-equal-of-cdr-of-member-equal
  (implies (no-duplicatesp-equal x)
    (not (member-equal a (cdr (member-equal a x)))))
  :hints (("Goal" :in-theory (enable no-duplicatesp member-equal))))
no-duplicatesp-equal-of-constheorem
(defthm no-duplicatesp-equal-of-cons
  (equal (no-duplicatesp-equal (cons a x))
    (and (not (member-equal a (double-rewrite x)))
      (no-duplicatesp-equal x)))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal))))
no-duplicatesp-equal-of-cons-no-splittheorem
(defthm no-duplicatesp-equal-of-cons-no-split
  (implies (not (member-equal a x))
    (equal (no-duplicatesp-equal (cons a x))
      (no-duplicatesp-equal x))))
no-duplicatesp-equal-of-appendtheorem
(defthm no-duplicatesp-equal-of-append
  (equal (no-duplicatesp-equal (append x y))
    (and (no-duplicatesp-equal x)
      (no-duplicatesp-equal y)
      (not (intersection-equal x y))))
  :hints (("Goal" :in-theory (enable append no-duplicatesp-equal))))
local
(local (defthm not-no-duplicatesp-equal-of-union-equal-when-not-no-duplicatesp-equal-arg2
    (implies (not (no-duplicatesp-equal y))
      (not (no-duplicatesp-equal (union-equal x y))))))
no-duplicatesp-equal-of-union-equaltheorem
(defthm no-duplicatesp-equal-of-union-equal
  (implies (no-duplicatesp-equal x)
    (equal (no-duplicatesp-equal (union-equal x y))
      (no-duplicatesp-equal y)))
  :hints (("Goal" :in-theory (enable union-equal no-duplicatesp-equal))))
no-duplicatesp-equal-of-set-difference-equaltheorem
(defthm no-duplicatesp-equal-of-set-difference-equal
  (implies (no-duplicatesp-equal x)
    (no-duplicatesp-equal (set-difference-equal x y)))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal))))
no-duplicatesp-equal-of-true-list-fixtheorem
(defthm no-duplicatesp-equal-of-true-list-fix
  (equal (no-duplicatesp-equal (true-list-fix x))
    (no-duplicatesp-equal x))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal))))
local
(local (defthm not-no-duplicatesp-equal-of-revappend-helper
    (implies (not (no-duplicatesp-equal y))
      (not (no-duplicatesp-equal (revappend x y))))
    :hints (("Goal" :in-theory (enable no-duplicatesp-equal revappend)))))
local
(local (defthm not-no-duplicatesp-equal-of-revappend-helper2
    (implies (and (member-equal a x) (member-equal a y))
      (not (no-duplicatesp-equal (revappend x y))))
    :hints (("Goal" :in-theory (enable no-duplicatesp-equal revappend)))))
no-duplicatesp-equal-of-revappendtheorem
(defthm no-duplicatesp-equal-of-revappend
  (equal (no-duplicatesp-equal (revappend x y))
    (and (no-duplicatesp-equal x)
      (no-duplicatesp-equal y)
      (not (intersection-equal x y))))
  :hints (("Goal" :in-theory (e/d (no-duplicatesp-equal revappend) (intersection-equal)))))
no-duplicatesp-equal-of-reversetheorem
(defthm no-duplicatesp-equal-of-reverse
  (equal (no-duplicatesp-equal (reverse x))
    (no-duplicatesp-equal x))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal))))
no-duplicatesp-equal-of-intersection-equaltheorem
(defthm no-duplicatesp-equal-of-intersection-equal
  (implies (no-duplicatesp-equal x)
    (no-duplicatesp-equal (intersection-equal x y)))
  :hints (("Goal" :in-theory (enable intersection-equal no-duplicatesp-equal))))
no-duplicatesp-equal-of-remove-equaltheorem
(defthm no-duplicatesp-equal-of-remove-equal
  (implies (no-duplicatesp-equal l)
    (no-duplicatesp-equal (remove-equal x l)))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal remove-equal))))