remove1-equal

other

(in-package "ACL2")

local

(local (include-book "len"))

in-theory

(in-theory (disable remove1-equal))

remove1-equal-of-niltheorem

(defthm remove1-equal-of-nil
  (equal (remove1-equal x nil) nil)
  :hints (("Goal" :in-theory (enable remove1-equal))))

remove1-equal-when-not-consptheorem

(defthmd remove1-equal-when-not-consp
  (implies (not (consp l)) (equal (remove1-equal x l) nil))
  :hints (("Goal" :in-theory (enable remove1-equal))))

remove1-equal-when-not-consp-cheaptheorem

(defthm remove1-equal-when-not-consp-cheap
  (implies (not (consp l)) (equal (remove1-equal x l) nil))
  :rule-classes ((:rewrite :backchain-limit-lst (0)))
  :hints (("Goal" :in-theory (enable remove1-equal))))

consp-of-remove1-equaltheorem

(defthm consp-of-remove1-equal
  (equal (consp (remove1-equal x l))
    (and (consp l)
      (not (and (equal 1 (len l)) (equal x (car l))))))
  :hints (("Goal" :in-theory (enable remove1-equal))))

remove1-equal-of-constheorem

(defthm remove1-equal-of-cons
  (equal (remove1-equal x (cons y l))
    (if (equal x y)
      l
      (cons y (remove1-equal x l))))
  :hints (("Goal" :in-theory (enable remove1-equal))))

remove1-equal-of-car-sametheorem

(defthm remove1-equal-of-car-same
  (equal (remove1-equal (car l) l) (cdr l))
  :hints (("Goal" :in-theory (enable remove1-equal))))

len-of-remove1-equal-lineartheorem

(defthm len-of-remove1-equal-linear
  (<= (len (remove1-equal x l)) (len l))
  :rule-classes ((:linear :trigger-terms ((len (remove1-equal x l)))))
  :hints (("Goal" :in-theory (enable remove1-equal))))

len-of-remove1-equal-linear-2theorem

(defthm len-of-remove1-equal-linear-2
  (<= (+ -1 (len l)) (len (remove1-equal x l)))
  :rule-classes ((:linear :trigger-terms ((len (remove1-equal x l)))))
  :hints (("Goal" :in-theory (enable remove1-equal))))

len-of-remove1-equaltheorem

(defthm len-of-remove1-equal
  (equal (len (remove1-equal x l))
    (if (member-equal x l)
      (+ -1 (len l))
      (len l)))
  :hints (("Goal" :in-theory (enable remove1-equal))))

true-listp-of-remove1-equaltheorem

(defthm true-listp-of-remove1-equal
  (implies (true-listp l) (true-listp (remove1-equal x l))))

true-list-fix-of-remove1-equaltheorem

(defthm true-list-fix-of-remove1-equal
  (equal (true-list-fix (remove1-equal x l))
    (remove1-equal x (true-list-fix l))))

remove1-equal-of-appendtheorem

(defthm remove1-equal-of-append
  (equal (remove1-equal x (append l1 l2))
    (if (member-equal x l1)
      (append (remove1-equal x l1) l2)
      (append l1 (remove1-equal x l2)))))

not-member-equal-of-remove1-equaltheorem

(defthm not-member-equal-of-remove1-equal
  (implies (not (member-equal x l))
    (not (member-equal x (remove1-equal y l))))
  :hints (("Goal" :in-theory (enable remove1-equal))))

member-equal-of-remove1-equal-when-not-equal-ifftheorem

(defthm member-equal-of-remove1-equal-when-not-equal-iff
  (implies (not (equal a b))
    (iff (member-equal a (remove1-equal b x))
      (member-equal a x))))

no-duplicatesp-equal-of-remove1-equaltheorem

(defthm no-duplicatesp-equal-of-remove1-equal
  (implies (no-duplicatesp-equal l)
    (no-duplicatesp-equal (remove1-equal x l)))
  :hints (("Goal" :in-theory (enable no-duplicatesp-equal remove1-equal))))

remove1-equal-of-remove1-equaltheorem

(defthm remove1-equal-of-remove1-equal
  (equal (remove1-equal x (remove1-equal y l))
    (remove1-equal y (remove1-equal x l)))
  :hints (("Goal" :in-theory (enable remove1-equal))))

remove1-equal-when-not-member-equaltheorem

(defthm remove1-equal-when-not-member-equal
  (implies (not (member-equal x l))
    (equal (remove1-equal x l) (true-list-fix l))))

<-of-acl2-count-of-remove1-equal-lineartheorem

(defthm <-of-acl2-count-of-remove1-equal-linear
  (implies (member-equal a x)
    (< (acl2-count (remove1-equal a x)) (acl2-count x)))
  :rule-classes ((:linear :trigger-terms ((acl2-count (remove1-equal a x)))))
  :hints (("Goal" :in-theory (enable remove1-equal))))

<=-of-acl2-count-of-remove1-equal-lineartheorem

(defthm <=-of-acl2-count-of-remove1-equal-linear
  (<= (acl2-count (remove1-equal a x)) (acl2-count x))
  :rule-classes ((:linear :trigger-terms ((acl2-count (remove1-equal a x)))))
  :hints (("Goal" :in-theory (enable remove1-equal))))

equal-of-acl2-count-of-remove1-equal-and-acl2-counttheorem

(defthm equal-of-acl2-count-of-remove1-equal-and-acl2-count
  (equal (equal (acl2-count (remove1-equal a x)) (acl2-count x))
    (if (member-equal a x)
      nil
      (equal (acl2-count (true-list-fix x)) (acl2-count x))))
  :hints (("Goal" :use (:instance <-of-acl2-count-of-remove1-equal-linear)
     :in-theory (disable <-of-acl2-count-of-remove1-equal-linear))))

Included Books