list-defthms

other

(in-package "ACL2")

include-book

(include-book "list-defuns")

local

(local (include-book "arithmetic/equalities" :dir :system))

initial-sublistp->initial-sublistp-equaltheorem

(defthm initial-sublistp->initial-sublistp-equal
  (equal (initial-sublistp a b) (initial-sublistp-equal a b)))

initial-sublistp-eq->initial-sublistp-equaltheorem

(defthm initial-sublistp-eq->initial-sublistp-equal
  (equal (initial-sublistp-eq a b)
    (initial-sublistp-equal a b)))

memberp->memberp-equaltheorem

(defthm memberp->memberp-equal
  (equal (memberp x l) (memberp-equal x l)))

memberp-eq->memberp-equaltheorem

(defthm memberp-eq->memberp-equal
  (equal (memberp-eq x l) (memberp-equal x l)))

local

(local (defthm occurrences-ac->occurrences-equal-ac
    (equal (occurrences-ac x l ac)
      (occurrences-equal-ac x l ac))))

occurrences->occurrences-equaltheorem

(defthm occurrences->occurrences-equal
  (equal (occurrences x l) (occurrences-equal x l)))

local

(local (defthm occurrences-eq-ac->occurrences-equal-ac
    (equal (occurrences-eq-ac x l ac)
      (occurrences-equal-ac x l ac))))

occurrences-eq->occurrences-equaltheorem

(defthm occurrences-eq->occurrences-equal
  (equal (occurrences-eq x l) (occurrences-equal x l)))

consp-appendtheorem

(defthm consp-append
  (equal (consp (append a b)) (or (consp a) (consp b)))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (consp a) (consp (append a b))))
    (:type-prescription :corollary (implies (consp b) (consp (append a b))))))

consp-revappendtheorem

(defthm consp-revappend
  (equal (consp (revappend a b)) (or (consp a) (consp b)))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (consp a) (consp (revappend a b))))
    (:type-prescription :corollary (implies (consp b) (consp (revappend a b))))))

consp-reversetheorem

(defthm consp-reverse
  (equal (consp (reverse a)) (consp a))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (consp a) (consp (reverse a))))))

local

(local (defthm consp-first-n-ac
    (equal (consp (first-n-ac i l ac))
      (if (zp i)
        (consp ac)
        t))
    :rule-classes ((:rewrite) (:type-prescription :corollary (implies (or (not (zp i)) (consp ac))
          (consp (first-n-ac i l ac)))))
    :hints (("Goal" :induct (first-n-ac i l ac)))))

local

(local (defthm consp-take
    (equal (consp (take n l)) (not (zp n)))
    :rule-classes ((:rewrite) (:type-prescription :corollary (implies (not (zp n)) (consp (take n l)))))))

consp-butlasttheorem

(defthm consp-butlast
  (equal (consp (butlast lst n))
    (not (zp (- (len lst) (nfix n)))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (natp n) (not (zp (- (len lst) n))))
        (consp (butlast lst n)))))
  :hints (("Goal" :do-not-induct t)))

consp-firstntheorem

(defthm consp-firstn
  (equal (consp (firstn n l)) (and (not (zp n)) (consp l)))
  :hints (("Goal" :expand (firstn n l)))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (not (zp n)) (consp l)) (consp (firstn n l))))))

consp-lasttheorem

(defthm consp-last
  (equal (consp (last l)) (consp l))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (consp l) (consp (last l))))))

consp-make-list-actheorem

(defthm consp-make-list-ac
  (equal (consp (make-list-ac n val ac))
    (or (not (zp n)) (consp ac)))
  :hints (("Goal" :expand (make-list-ac n val ac)))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (not (zp n)) (consp ac))
        (consp (make-list-ac n val ac))))))

consp-member-equaltheorem

(defthm consp-member-equal
  (or (consp (member-equal x l))
    (equal (member-equal x l) nil))
  :rule-classes ((:type-prescription) (:rewrite :corollary (iff (not (consp (member-equal x l)))
        (equal (member-equal x l) nil)))))

local

(local (defthm nthcdr-nil
    (implies (and (integerp n) (<= 0 n)) (not (nthcdr n nil)))))

consp-nthcdrtheorem

(defthm consp-nthcdr
  (iff (consp (nthcdr n l)) (< (nfix n) (len l)))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (< (nfix n) (len l)) (consp (nthcdr n l))))))

consp-nth-segtheorem

(defthm consp-nth-seg
  (implies (<= (+ i j) (len l))
    (equal (consp (nth-seg i j l)) (and (consp l) (not (zp j)))))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (and (consp l) (not (zp j)) (<= (+ i j) (len l)))
        (consp (nth-seg i j l))))))

consp-put-nththeorem

(defthm consp-put-nth
  (equal (consp (put-nth n v l)) (consp l))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (consp l) (consp (put-nth n v l))))))

consp-put-segtheorem

(defthm consp-put-seg
  (equal (consp (put-seg i seg l)) (consp l))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (consp l) (consp (put-seg i seg l))))))

consp-subseqtheorem

(defthm consp-subseq
  (implies (and (true-listp list)
      (integerp start)
      (<= 0 start)
      (or (null end) (and (integerp end) (<= 0 end))))
    (iff (consp (subseq list start end))
      (< start
        (if (null end)
          (len list)
          end))))
  :hints (("Goal" :do-not-induct t :in-theory (disable take))))

true-listp-append-rewritetheorem

(defthm true-listp-append-rewrite
  (equal (true-listp (append a b)) (true-listp b))
  :rule-classes ((:rewrite)))

true-listp-revappendtheorem

(defthm true-listp-revappend
  (equal (true-listp (revappend a b)) (true-listp b))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp b) (true-listp (revappend a b))))))

true-listp-reversetheorem

(defthm true-listp-reverse
  (implies (listp a) (true-listp (reverse a)))
  :rule-classes (:type-prescription))

local

(local (defthm true-listp-first-n-ac-rewrite
    (implies (true-listp ac) (true-listp (first-n-ac i l ac)))
    :rule-classes (:rewrite)
    :hints (("Goal" :induct (first-n-ac i l ac)))))

local

(local (defthm true-listp-take-rewrite
    (true-listp (take n l))
    :rule-classes (:rewrite)))

true-listp-butlasttheorem

(defthm true-listp-butlast
  (true-listp (butlast lst n))
  :rule-classes (:rewrite :type-prescription))

true-listp-lasttheorem

(defthm true-listp-last
  (equal (true-listp (last l)) (true-listp l))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp l) (true-listp (last l))))))

true-listp-make-list-actheorem

(defthm true-listp-make-list-ac
  (equal (true-listp (make-list-ac n val ac)) (true-listp ac))
  :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp ac)
        (true-listp (make-list-ac n val ac))))))

true-listp-member-equaltheorem

(defthm true-listp-member-equal
  (implies (true-listp l) (true-listp (member-equal x l)))
  :rule-classes (:rewrite :type-prescription))

true-listp-nthcdrtheorem

(defthm true-listp-nthcdr
  (implies (true-listp l) (true-listp (nthcdr n l)))
  :hints (("Goal" :induct (nthcdr n l)))
  :rule-classes (:rewrite :type-prescription))

true-listp-put-nththeorem

(defthm true-listp-put-nth
  (implies (true-listp l) (true-listp (put-nth n v l)))
  :rule-classes (:rewrite :type-prescription))

true-listp-put-segtheorem

(defthm true-listp-put-seg
  (implies (true-listp l) (true-listp (put-seg i seg l)))
  :rule-classes (:rewrite :type-prescription))

local

(local (defthm true-listp-subseq-list
    (true-listp (subseq-list lst start end))
    :hints (("Goal" :do-not-induct t :in-theory (disable take)))
    :rule-classes (:rewrite :type-prescription)))

true-listp-subseqtheorem

(defthm true-listp-subseq
  (implies (true-listp seq)
    (true-listp (subseq seq start end)))
  :hints (("Goal" :do-not-induct t :in-theory (disable subseq-list)))
  :rule-classes (:rewrite :type-prescription))

local

(local (defthm naturalp-occurrences-equal-ac
    (implies (and (integerp acc) (<= 0 acc))
      (and (integerp (occurrences-equal-ac item lst acc))
        (<= 0 (occurrences-equal-ac item lst acc))))))

naturalp-occurrences-equaltheorem

(defthm naturalp-occurrences-equal
  (and (integerp (occurrences-equal item lst))
    (<= 0 (occurrences-equal item lst)))
  :rule-classes (:rewrite :type-prescription))

local

(local (defthm naturalp-position-equal-ac
    (implies (and (integerp acc) (<= 0 acc) (member-equal item lst))
      (and (integerp (position-equal-ac item lst acc))
        (<= 0 (position-equal-ac item lst acc))))))

naturalp-position-equaltheorem

(defthm naturalp-position-equal
  (implies (member-equal item lst)
    (and (integerp (position-equal item lst))
      (<= 0 (position-equal item lst))))
  :rule-classes (:rewrite :type-prescription))

local

(local (defthm nth-seg-non-recursive
    (equal (nth-seg i j l) (firstn j (nthcdr i l)))))

local

(local (defthm put-seg-non-recursive
    (implies (and (true-listp l) (integerp i) (>= i 0))
      (equal (put-seg i seg l)
        (append (firstn i l)
          (firstn (nfix (- (len l) i)) seg)
          (nthcdr (+ i (min (nfix (- (len l) i)) (len seg))) l))))
    :hints (("Goal" :induct (put-seg i seg l)))))

local

(local (in-theory (disable nth-seg-non-recursive put-seg-non-recursive)))

positive-len-fwd-to-consptheorem

(defthm positive-len-fwd-to-consp
  (implies (< 0 (len l)) (consp l))
  :rule-classes :forward-chaining)

len-appendtheorem

(defthm len-append
  (equal (len (append a b)) (+ (len a) (len b))))

len-revappendtheorem

(defthm len-revappend
  (equal (len (revappend a b)) (+ (len a) (len b))))

len-reversetheorem

(defthm len-reverse (equal (len (reverse a)) (len a)))

local

(local (defthm len-first-n-ac
    (equal (len (first-n-ac n l ac)) (+ (nfix n) (len ac)))
    :hints (("Goal" :induct (first-n-ac n l ac)))))

local

(local (defthm len-take (equal (len (take n l)) (nfix n))))

len-butlasttheorem

(defthm len-butlast
  (implies (and (integerp n) (<= 0 n))
    (equal (len (butlast lst n))
      (if (<= (len lst) n)
        0
        (- (len lst) n))))
  :hints (("Goal" :do-not-induct t :in-theory (disable take))))

len-firstntheorem

(defthm len-firstn
  (equal (len (firstn n l))
    (if (<= (nfix n) (len l))
      (nfix n)
      (len l)))
  :hints (("Goal" :induct (firstn n l))))

len-lasttheorem

(defthm len-last
  (equal (len (last l))
    (if (consp l)
      1
      0))
  :hints (("Goal" :induct (last l))))

len-make-list-actheorem

(defthm len-make-list-ac
  (equal (len (make-list-ac n val ac)) (+ (nfix n) (len ac)))
  :hints (("Goal" :induct (make-list-ac n val ac))))

len-member-equaltheorem

(defthm len-member-equal
  (not (< (len l) (len (member-equal x l))))
  :rule-classes (:rewrite :linear))

len-nthcdrtheorem

(defthm len-nthcdr
  (equal (len (nthcdr n l))
    (if (<= (nfix n) (len l))
      (- (len l) (nfix n))
      0))
  :hints (("Goal" :induct (nthcdr n l))))

len-nth-segtheorem

(defthm len-nth-seg
  (implies (<= (+ i j) (len l))
    (equal (len (nth-seg i j l))
      (min (nfix j) (max (- (len l) (nfix i)) 0))))
  :hints (("Goal" :do-not-induct t
     :in-theory (union-theories (set-difference-theories (current-theory :here)
         '((:definition nth-seg)))
       '(nth-seg-non-recursive)))))

len-put-nththeorem

(defthm len-put-nth (equal (len (put-nth n v l)) (len l)))

len-put-segtheorem

(defthm len-put-seg
  (implies (and (integerp i) (not (< i 0)))
    (equal (len (put-seg i seg l)) (len l))))

local

(local (defthm occurrences-equal-ac+1
    (implies (acl2-numberp ac)
      (equal (occurrences-equal-ac x l (+ 1 ac))
        (+ 1 (occurrences-equal-ac x l ac))))))

local

(local (in-theory (disable occurrences-equal-ac+1)))

local

(local (defthm len-remove-equal-ac
    (implies (acl2-numberp ac)
      (equal (len (remove-equal x l))
        (+ ac (- (len l) (occurrences-equal-ac x l ac)))))
    :rule-classes nil
    :hints (("Goal" :induct (remove-equal x l)
       :in-theory (enable occurrences-equal-ac+1)) ("Subgoal *1/2'''" :expand ((occurrences-equal-ac l1 (cons l1 l2) ac))))))

len-remove-equaltheorem

(defthm len-remove-equal
  (equal (len (remove-equal x l))
    (- (len l) (occurrences-equal x l)))
  :hints (("Goal" :do-not-induct t
     :use ((:instance len-remove-equal-ac (ac 0))))))

len-subseqtheorem

(defthm len-subseq
  (implies (and (true-listp l)
      (integerp start)
      (<= 0 start)
      (or (and (integerp end) (<= start end)) (null end)))
    (equal (len (subseq l start end))
      (if (null end)
        (len (nthcdr start l))
        (- (nfix end) (nfix start)))))
  :hints (("Goal" :do-not-induct t :in-theory (disable take))))

len-update-nth1theorem

(defthm len-update-nth1
  (equal (len (update-nth n val l))
    (if (< (nfix n) (len l))
      (len l)
      (+ 1 (nfix n))))
  :hints (("Goal" :induct (update-nth n val l))))

local

(local (defthm leq-occurrences-equal-ac-len
    (implies (acl2-numberp ac)
      (not (< (+ (len l) ac) (occurrences-equal-ac x l ac))))
    :rule-classes nil))

leq-occurrences-equal-lentheorem

(defthm leq-occurrences-equal-len
  (not (< (len l) (occurrences-equal x l)))
  :rule-classes (:rewrite :linear)
  :hints (("Goal" :do-not-induct t
     :use ((:instance leq-occurrences-equal-ac-len (ac 0))))))

local

(local (defthm leq-position-equal-ac-len
    (implies (and (acl2-numberp ac) (member-equal x l))
      (not (< (+ (len l) ac) (position-equal-ac x l ac))))
    :rule-classes nil))

leq-position-equal-lentheorem

(defthm leq-position-equal-len
  (implies (member-equal x l)
    (not (< (len l) (position-equal x l))))
  :rule-classes (:rewrite :linear)
  :hints (("Goal" :do-not-induct t
     :use ((:instance leq-position-equal-ac-len (ac 0))))))

append-right-idtheorem

(defthm append-right-id
  (implies (true-listp a) (equal (append a nil) a)))

associativity-of-appendtheorem

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

append-firstn-nthcdrtheorem

(defthm append-firstn-nthcdr
  (implies (true-listp l)
    (equal (append (firstn n l) (nthcdr n l)) l)))

revappend-binary-appendtheorem

(defthm revappend-binary-append
  (equal (revappend (binary-append a b) c)
    (revappend b (revappend a c))))

binary-append-revappendtheorem

(defthm binary-append-revappend
  (equal (binary-append (revappend a b) c)
    (revappend a (binary-append b c))))

reverse-appendtheorem

(defthm reverse-append
  (implies (and (listp a) (listp b))
    (equal (reverse (append a b))
      (append (reverse b) (reverse a))))
  :hints (("Goal" :do-not-induct t)))

revappend-revappendtheorem

(defthm revappend-revappend
  (equal (revappend (revappend a b) c)
    (revappend b (binary-append a c))))

reverse-reversetheorem

(defthm reverse-reverse
  (implies (true-listp l) (equal (reverse (reverse l)) l))
  :hints (("Goal" :do-not-induct t)))

local

(local (defthm first-n-ac-len
    (implies (and (true-listp ac) (true-listp l) (eql (len l) n))
      (equal (first-n-ac n l ac) (revappend ac l)))
    :hints (("Goal" :induct t))))

local

(local (defthm take-len
    (implies (true-listp l) (equal (take (len l) l) l))))

local

(local (defthm first-n-ac-append1
    (implies (<= n (len a))
      (equal (first-n-ac n (append a b) ac) (first-n-ac n a ac)))
    :hints (("Goal" :induct (first-n-ac n a ac)))))

local

(local (defthm take-append1
    (implies (<= n (len a))
      (equal (take n (append a b)) (take n a)))))

butlast-append1-crocktheorem

(defthm butlast-append1-crock
  (implies (and (true-listp a) (<= (+ (len a) i) i))
    (equal nil a))
  :rule-classes nil)

butlast-append1theorem

(defthm butlast-append1
  (implies (true-listp a)
    (equal (butlast (append a b) (len b)) a))
  :hints (("Goal" :do-not-induct t
     :use ((:instance butlast-append1-crock (i (len b))))
     :in-theory (disable take))))

firstn-with-large-indextheorem

(defthm firstn-with-large-index
  (implies (and (<= (len l) (nfix n)) (true-listp l))
    (equal (firstn n l) l)))

firstn-appendtheorem

(defthm firstn-append
  (equal (firstn n (append a b))
    (if (<= (nfix n) (len a))
      (firstn n a)
      (append a (firstn (- n (len a)) b)))))

firstn-firstntheorem

(defthm firstn-firstn
  (equal (firstn i (firstn j l))
    (if (< (nfix i) (nfix j))
      (firstn i l)
      (firstn j l))))

firstn-make-list-actheorem

(defthm firstn-make-list-ac
  (equal (firstn i (make-list-ac j v ac))
    (if (< (nfix i) (nfix j))
      (make-list-ac i v nil)
      (make-list-ac j v (firstn (- i (nfix j)) ac)))))

local

(local (defthm firstn-cons
    (equal (firstn n (cons a l))
      (if (zp n)
        nil
        (cons a (firstn (1- n) l))))))

firstn-put-nththeorem

(defthm firstn-put-nth
  (equal (firstn i (put-nth j v l))
    (if (<= (nfix i) (nfix j))
      (firstn i l)
      (put-nth j v (firstn i l))))
  :rule-classes ((:rewrite :corollary (implies (<= (nfix i) (nfix j))
       (equal (firstn i (put-nth j v l)) (firstn i l))))))

member-equal-appendtheorem

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

member-equal-make-list-ac-instancetheorem

(defthm member-equal-make-list-ac-instance
  (implies (not (zp n))
    (member-equal x (make-list-ac n x ac)))
  :hints (("Goal" :induct (make-list-ac n x ac))))

consp-member-equal-make-list-actheorem

(defthm consp-member-equal-make-list-ac
  (implies (not (zp n))
    (consp (member-equal x (make-list-ac n x ac))))
  :hints (("Goal" :induct (make-list-ac n x ac))))

member-equal-make-list-actheorem

(defthm member-equal-make-list-ac
  (implies (not (member-equal x ac))
    (iff (member-equal x (make-list-ac n y ac))
      (and (not (zp n)) (equal x y)))))

member-equal-car-lasttheorem

(defthm member-equal-car-last
  (implies (consp l) (member-equal (car (last l)) l)))

member-equal-nththeorem

(defthm member-equal-nth
  (implies (< (nfix n) (len l)) (member-equal (nth n l) l))
  :hints (("Goal" :in-theory (enable nth))))

member-equal-put-nththeorem

(defthm member-equal-put-nth
  (implies (< (nfix n) (len l))
    (member-equal x (put-nth n x l))))

consp-member-equal-remove-equaltheorem

(defthm consp-member-equal-remove-equal
  (iff (consp (member-equal x (remove-equal y l)))
    (if (equal x y)
      nil
      (consp (member-equal x l))))
  :hints (("Goal" :induct (remove-equal y l))))

member-equal-remove-equaltheorem

(defthm member-equal-remove-equal
  (iff (member-equal x (remove-equal y l))
    (if (equal x y)
      nil
      (member-equal x l))))

consp-member-equal-remove-duplicates-equaltheorem

(defthm consp-member-equal-remove-duplicates-equal
  (iff (consp (member-equal x (remove-duplicates-equal l)))
    (consp (member-equal x l)))
  :hints (("Goal" :induct (remove-duplicates-equal l))))

member-equal-remove-duplicates-equaltheorem

(defthm member-equal-remove-duplicates-equal
  (iff (member-equal x (remove-duplicates-equal l))
    (member-equal x l)))

member-equal-revappendtheorem

(defthm member-equal-revappend
  (iff (member-equal x (revappend a b))
    (or (member-equal x a) (member-equal x b)))
  :hints (("Goal" :induct (revappend a b))))

member-equal-reversetheorem

(defthm member-equal-reverse
  (iff (member-equal x (reverse l)) (member-equal x l)))

member-equal-update-nththeorem

(defthm member-equal-update-nth
  (member-equal x (update-nth n x l)))

memberp-equal-appendtheorem

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

memberp-equal-make-list-actheorem

(defthm memberp-equal-make-list-ac
  (implies (not (memberp-equal x ac))
    (iff (memberp-equal x (make-list-ac n y ac))
      (and (not (zp n)) (equal x y)))))

memberp-equal-car-lasttheorem

(defthm memberp-equal-car-last
  (implies (consp l) (memberp-equal (car (last l)) l)))

memberp-equal-nththeorem

(defthm memberp-equal-nth
  (implies (< (nfix n) (len l)) (memberp-equal (nth n l) l))
  :hints (("Goal" :in-theory (enable nth))))

memberp-equal-put-nththeorem

(defthm memberp-equal-put-nth
  (implies (< (nfix n) (len l))
    (memberp-equal x (put-nth n x l))))

memberp-equal-remove-equaltheorem

(defthm memberp-equal-remove-equal
  (iff (memberp-equal x (remove-equal y l))
    (if (equal x y)
      nil
      (memberp-equal x l))))

memberp-equal-remove-duplicates-equaltheorem

(defthm memberp-equal-remove-duplicates-equal
  (iff (memberp-equal x (remove-duplicates-equal l))
    (memberp-equal x l)))

memberp-equal-revappendtheorem

(defthm memberp-equal-revappend
  (iff (memberp-equal x (revappend a b))
    (or (memberp-equal x a) (memberp-equal x b)))
  :hints (("Goal" :induct (revappend a b))))

consp-member-equal-revappendtheorem

(defthm consp-member-equal-revappend
  (iff (consp (member-equal x (revappend a b)))
    (or (consp (member-equal x a)) (consp (member-equal x b))))
  :hints (("Goal" :induct (revappend a b))))

memberp-equal-reversetheorem

(defthm memberp-equal-reverse
  (iff (memberp-equal x (reverse l)) (memberp-equal x l))
  :hints (("Goal" :do-not-induct t)))

memberp-equal-update-nththeorem

(defthm memberp-equal-update-nth
  (memberp-equal x (update-nth n x l)))

initial-sublistp-equal-reflexivetheorem

(defthm initial-sublistp-equal-reflexive
  (initial-sublistp-equal l l))

initial-sublistp-equal-niltheorem

(defthm initial-sublistp-equal-nil
  (initial-sublistp-equal nil l))

no-duplicatesp-equal-remove-duplicates-equaltheorem

(defthm no-duplicatesp-equal-remove-duplicates-equal
  (no-duplicatesp-equal (remove-duplicates-equal l))
  :hints (("Goal" :induct (remove-duplicates-equal l))))

nth-of-niltheorem

(defthm nth-of-nil (equal (nth n nil) nil))

nth-with-large-indextheorem

(defthm nth-with-large-index
  (implies (<= (len l) (nfix n)) (equal (nth n l) nil)))

nth-appendtheorem

(defthm nth-append
  (equal (nth n (append a b))
    (if (< (nfix n) (len a))
      (nth n a)
      (nth (- (nfix n) (len a)) b))))

nth-revappendtheorem

(defthm nth-revappend
  (equal (nth n (revappend a b))
    (if (< (nfix n) (len a))
      (nth (- (len a) (1+ (nfix n))) a)
      (nth (- (nfix n) (len a)) b)))
  :hints (("Goal" :induct (revappend a b))))

nth-reversetheorem

(defthm nth-reverse
  (implies (and (integerp n) (<= 0 n))
    (equal (nth n (reverse a))
      (if (< n (len a))
        (nth (- (len a) (1+ n)) a)
        nil))))

xfirstnfunction

(defun xfirstn
  (n l)
  (declare (xargs :guard (and (integerp n) (<= 0 n) (true-listp l))))
  (cond ((zp n) nil)
    (t (cons (car l) (xfirstn (1- n) (cdr l))))))

len-xfirstntheorem

(defthm len-xfirstn (equal (len (xfirstn n x)) (nfix n)))

nth-xfirstntheorem

(defthm nth-xfirstn
  (equal (nth i (xfirstn n l))
    (if (<= (nfix n) (len l))
      (if (< (nfix i) (nfix n))
        (nth i l)
        nil)
      (if (< (nfix i) (len l))
        (nth i l)
        nil))))

first-n-ac-non-recursivetheorem

(defthm first-n-ac-non-recursive
  (implies (true-listp ac)
    (equal (first-n-ac n l ac) (revappend ac (xfirstn n l)))))

take-is-xfirstntheorem

(defthmd take-is-xfirstn (equal (take n l) (xfirstn n l)))

local

(local (in-theory (enable take-is-xfirstn)))

local

(local (in-theory (disable take)))

nth-taketheorem

(defthm nth-take
  (equal (nth i (take n l))
    (if (<= (nfix n) (len l))
      (if (< (nfix i) (nfix n))
        (nth i l)
        nil)
      (if (< (nfix i) (len l))
        (nth i l)
        nil)))
  :hints (("Goal" :do-not-induct t)))

nth-butlasttheorem

(defthm nth-butlast
  (implies (and (integerp i) (<= 0 i) (integerp n) (<= 0 n))
    (equal (nth i (butlast l n))
      (if (< i (- (len l) n))
        (nth i l)
        nil)))
  :hints (("Goal" :do-not-induct t :in-theory (disable revappend))))

car-nthcdrtheorem

(defthm car-nthcdr (equal (car (nthcdr n l)) (nth n l)))

cdr-over-nthcdrtheorem

(defthmd cdr-over-nthcdr
  (equal (cdr (nthcdr n l)) (nthcdr n (cdr l))))

local

(local (in-theory (enable cdr-over-nthcdr)))

nth-nthcdrtheorem

(defthm nth-nthcdr
  (equal (nth i (nthcdr j l)) (nth (+ (nfix j) (nfix i)) l)))

nth-subseqtheorem

(defthm nth-subseq
  (implies (and (true-listp l)
      (integerp start)
      (<= 0 start)
      (or (and (integerp end) (<= start end)) (null end))
      (integerp n)
      (<= 0 n))
    (equal (nth n (subseq l start end))
      (if (null end)
        (nth n (nthcdr start l))
        (nth n (take (- end start) (nthcdr start l))))))
  :hints (("Goal" :do-not-induct t :in-theory (disable revappend))))

nth-firstntheorem

(defthm nth-firstn
  (equal (nth i (firstn j l))
    (if (< (nfix i) (nfix j))
      (nth i l)
      nil))
  :hints (("Goal" :induct (and (nth i (firstn j l)) (nth i l) (firstn j l)))))

nth-make-list-actheorem

(defthm nth-make-list-ac
  (equal (nth i (make-list-ac j val ac))
    (if (< (nfix i) (nfix j))
      val
      (nth (- i (nfix j)) ac)))
  :hints (("Goal" :induct (make-list-ac j val ac))))

nth-nth-segtheorem

(defthm nth-nth-seg
  (equal (nth n (nth-seg i j l))
    (if (< (nfix n) (nfix j))
      (nth (+ (nfix i) (nfix n)) l)
      nil))
  :hints (("Goal" :do-not-induct t
     :in-theory (union-theories (set-difference-theories (current-theory :here)
         '((:definition nth-seg)))
       '(nth-seg-non-recursive)))))

nth-put-nththeorem

(defthm nth-put-nth
  (equal (nth i (put-nth j v l))
    (if (< (nfix i) (len l))
      (if (equal (nfix i) (nfix j))
        v
        (nth i l))
      (nth i l))))

local

(local (defthm nth-put-seg-helper-1
    (implies (and (integerp i)
        (integerp n)
        (< (len l) i)
        (not (< n (len l))))
      (not (nth (+ i n (- (len l))) l)))
    :hints (("Goal" :use (:instance nth-with-large-index
         (l l)
         (n (+ i n (- (len l)))))
       :in-theory (disable nth-with-large-index)))))

nth-put-segtheorem

(defthm nth-put-seg
  (implies (and (integerp i) (not (< i 0)))
    (equal (nth n (put-seg i seg l))
      (if (< (nfix n) i)
        (nth n l)
        (if (< (nfix n) (+ i (min (max (- (len l) i) 0) (len seg))))
          (nth (- (nfix n) i) seg)
          (nth n l))))))

local

(local (defthm nth-position-equal-ac
    (implies (member-equal x l)
      (equal (nth (- (position-equal-ac x l ac) ac) l) x))
    :rule-classes nil))

nth-position-equaltheorem

(defthm nth-position-equal
  (implies (member-equal x l)
    (equal (nth (position-equal x l) l) x))
  :hints (("Goal" :use ((:instance nth-position-equal-ac (ac 0))))))

nthcdr-with-large-indextheorem

(defthm nthcdr-with-large-index
  (implies (and (<= (len l) (nfix n)) (true-listp l))
    (equal (nthcdr n l) nil)))

nthcdr-appendtheorem

(defthm nthcdr-append
  (equal (nthcdr n (append a b))
    (if (<= (nfix n) (len a))
      (append (nthcdr n a) b)
      (nthcdr (- n (len a)) b))))

nthcdr-firstntheorem

(defthm nthcdr-firstn
  (equal (nthcdr i (firstn j l))
    (if (<= (nfix j) (nfix i))
      nil
      (firstn (- (nfix j) (nfix i)) (nthcdr i l))))
  :hints (("Goal" :induct t)))

nthcdr-make-list-actheorem

(defthm nthcdr-make-list-ac
  (equal (nthcdr i (make-list-ac j v ac))
    (if (<= (nfix j) (nfix i))
      (nthcdr (- (nfix i) (nfix j)) ac)
      (make-list-ac (- (nfix j) (nfix i)) v ac)))
  :hints (("Goal" :induct t :expand (make-list-ac (+ (- i) j) v ac))))

nthcdr-nthcdrtheorem

(defthm nthcdr-nthcdr
  (equal (nthcdr i (nthcdr j l))
    (nthcdr (+ (nfix j) (nfix i)) l)))

nthcdr-nth-segtheorem

(defthm nthcdr-nth-seg
  (equal (nthcdr n (nth-seg i j l))
    (nth-seg (+ (nfix i) (nfix n))
      (max (- (nfix j) (nfix n)) 0)
      l))
  :hints (("Goal" :do-not-induct t
     :in-theory (union-theories (set-difference-theories (current-theory :here)
         '((:definition nth-seg)))
       '(nth-seg-non-recursive)))))

nthcdr-put-nththeorem

(defthm nthcdr-put-nth
  (equal (nthcdr i (put-nth j v l))
    (if (< (nfix j) (nfix i))
      (nthcdr i l)
      (put-nth (- (nfix j) (nfix i)) v (nthcdr i l))))
  :hints (("Goal" :induct t))
  :rule-classes ((:rewrite :corollary (implies (< (nfix j) (nfix i))
       (equal (nthcdr i (put-nth j v l)) (nthcdr i l))))))

local

(local (defun xoccurrences-equal
    (x l)
    (declare (xargs :guard (and (true-listp l) (or (symbolp x) (symbol-listp l)))))
    (cond ((endp l) 0)
      ((eql x (car l)) (1+ (xoccurrences-equal x (cdr l))))
      (t (xoccurrences-equal x (cdr l))))))

local

(local (defthm occurrences-equal-ac-equals-xoccurrences-equal
    (implies (integerp ac)
      (equal (occurrences-equal-ac x l ac)
        (+ (xoccurrences-equal x l) ac)))))

local

(local (defun xposition-equal
    (x l)
    (declare (xargs :guard (and (true-listp l) (or (symbolp x) (symbol-listp l)))))
    (cond ((endp l) nil)
      ((eq x (car l)) 0)
      (t (let ((n (xposition-equal x (cdr l))))
          (and n (1+ n)))))))

local

(local (defthm position-equal-ac-equals-xposition-equal1
    (implies (integerp ac)
      (iff (position-equal-ac x l ac) (xposition-equal x l)))))

local

(local (defthm position-equal-ac-equals-xposition-equal2
    (implies (and (integerp ac) (position-equal-ac x l ac))
      (equal (position-equal-ac x l ac)
        (+ (xposition-equal x l) ac)))))

local

(local (defthm position-equal-ac-iff-member-equal
    (implies (integerp ac)
      (iff (position-equal-ac x l ac) (member-equal x l)))))

local

(local (defthm equal-occurrences-equal-ac-zero
    (implies (and (not (member-equal x l)) (integerp acc))
      (equal (occurrences-equal-ac x l acc) acc))))

equal-occurrences-equal-zerotheorem

(defthm equal-occurrences-equal-zero
  (implies (not (member-equal x l))
    (equal (occurrences-equal x l) 0)))

local

(local (defthm equal-occurrences-equal-ac-one
    (implies (and (member-equal x l)
        (no-duplicatesp-equal l)
        (integerp acc))
      (equal (occurrences-equal-ac x l acc) (+ acc 1)))))

equal-occurrences-equal-onetheorem

(defthm equal-occurrences-equal-one
  (implies (and (member-equal x l) (no-duplicatesp-equal l))
    (equal (occurrences-equal x l) 1)))

local

(local (defthm xoccurrences-equal-append
    (implies (integerp ac)
      (equal (xoccurrences-equal x (append a b))
        (+ (xoccurrences-equal x a) (xoccurrences-equal x b))))))

occurrences-equal-appendtheorem

(defthm occurrences-equal-append
  (equal (occurrences-equal x (append a b))
    (+ (occurrences-equal x a) (occurrences-equal x b))))

local

(local (defthm xoccurrences-equal-revappend
    (equal (xoccurrences-equal x (revappend a b))
      (+ (xoccurrences-equal x a) (xoccurrences-equal x b)))))

occurrences-equal-reversetheorem

(defthm occurrences-equal-reverse
  (equal (occurrences-equal x (reverse a))
    (occurrences-equal x a)))

local

(local (defthm leq-xoccurrences-equal-firstn
    (<= (xoccurrences-equal x (firstn n l))
      (xoccurrences-equal x l))))

occurrences-equal-firstntheorem

(defthm occurrences-equal-firstn
  (<= (occurrences-equal x (firstn n l))
    (occurrences-equal x l))
  :rule-classes :linear)

local

(local (defthm xoccurrences-equal-firstn-xposition-equal
    (implies (member-equal x l)
      (equal (xoccurrences-equal x (firstn (xposition-equal x l) l))
        0))))

occurrences-equal-firstn-position-equaltheorem

(defthm occurrences-equal-firstn-position-equal
  (implies (member-equal x l)
    (equal (occurrences-equal x (firstn (position-equal x l) l))
      0))
  :hints (("Goal" :do-not-induct t)))

local

(local (defthm xoccurrences-equal-make-list-ac
    (equal (xoccurrences-equal x (make-list-ac n val ac))
      (if (eql x val)
        (+ (nfix n) (xoccurrences-equal x ac))
        (xoccurrences-equal x ac)))
    :hints (("Goal" :induct (make-list-ac n val ac)))))

occurrences-equal-make-list-actheorem

(defthm occurrences-equal-make-list-ac
  (equal (occurrences-equal x (make-list-ac n val ac))
    (if (eql x val)
      (+ (nfix n) (occurrences-equal x ac))
      (occurrences-equal x ac)))
  :hints (("Goal" :do-not-induct t)))

local

(local (defthm xoccurrences-equal-member-equal
    (implies (member-equal x l)
      (equal (xoccurrences-equal x (member-equal x l))
        (xoccurrences-equal x l)))))

occurrences-equal-member-equaltheorem

(defthm occurrences-equal-member-equal
  (implies (member-equal x l)
    (equal (occurrences-equal x (member-equal x l))
      (occurrences-equal x l))))

local

(local (defthm leq-xoccurrences-equal-nthcdr
    (<= (xoccurrences-equal x (nthcdr n l))
      (xoccurrences-equal x l))))

occurrences-equal-nthcdrtheorem

(defthm occurrences-equal-nthcdr
  (<= (occurrences-equal x (nthcdr n l))
    (occurrences-equal x l))
  :rule-classes :linear)

local

(local (defthm xoccurrences-equal-nthcdr-xposition-equal
    (implies (member-equal x l)
      (equal (xoccurrences-equal x (nthcdr (xposition-equal x l) l))
        (xoccurrences-equal x l)))))

occurrences-equal-nthcdr-position-equaltheorem

(defthm occurrences-equal-nthcdr-position-equal
  (implies (member-equal x l)
    (equal (occurrences-equal x (nthcdr (position-equal x l) l))
      (occurrences-equal x l))))

local

(local (defthm xoccurrences-equal-put-nth
    (equal (xoccurrences-equal x (put-nth n v l))
      (if (< (nfix n) (len l))
        (if (equal x v)
          (if (equal x (nth n l))
            (xoccurrences-equal x l)
            (1+ (xoccurrences-equal x l)))
          (if (equal x (nth n l))
            (1- (xoccurrences-equal x l))
            (xoccurrences-equal x l)))
        (xoccurrences-equal x l)))
    :hints (("Goal" :induct (put-nth n v l) :in-theory (enable nth)))))

occurrences-equal-put-nththeorem

(defthm occurrences-equal-put-nth
  (equal (occurrences-equal x (put-nth n v l))
    (if (< (nfix n) (len l))
      (if (equal x v)
        (if (equal x (nth n l))
          (occurrences-equal x l)
          (1+ (occurrences-equal x l)))
        (if (equal x (nth n l))
          (1- (occurrences-equal x l))
          (occurrences-equal x l)))
      (occurrences-equal x l)))
  :hints (("Goal" :do-not-induct t)))

local

(local (defthm xoccurrences-equal-remove-equal
    (equal (xoccurrences-equal x (remove-equal y l))
      (if (equal x y)
        0
        (xoccurrences-equal x l)))
    :hints (("Goal" :induct (remove-equal y l)))))

occurrences-equal-remove-equaltheorem

(defthm occurrences-equal-remove-equal
  (equal (occurrences-equal x (remove-equal y l))
    (if (equal x y)
      0
      (occurrences-equal x l)))
  :hints (("Goal" :do-not-induct t)))

local

(local (defthm xoccurrences-equal-remove-duplicates-equal
    (<= (xoccurrences-equal x (remove-duplicates-equal l)) 1)))

occurrences-equal-remove-duplicates-equaltheorem

(defthm occurrences-equal-remove-duplicates-equal
  (<= (occurrences-equal x (remove-duplicates-equal l)) 1)
  :rule-classes (:rewrite :linear))

position-equal-iff-member-equaltheorem

(defthm position-equal-iff-member-equal
  (implies (not (stringp lst))
    (iff (position-equal item lst) (member-equal item lst)))
  :hints (("Goal" :do-not-induct t)))

local

(local (defthm xposition-equal-append
    (equal (xposition-equal x (append a b))
      (if (member-equal x a)
        (xposition-equal x a)
        (if (member-equal x b)
          (+ (len a) (xposition-equal x b))
          nil)))))

position-equal-appendtheorem

(defthm position-equal-append
  (implies (not (stringp b))
    (equal (position-equal x (append a b))
      (if (member-equal x a)
        (position-equal x a)
        (if (member-equal x b)
          (+ (len a) (position-equal x b))
          nil))))
  :hints (("Goal" :do-not-induct t)))

put-nth-with-large-indextheorem

(defthm put-nth-with-large-index
  (implies (and (true-listp l) (<= (len l) (nfix n)))
    (equal (put-nth n v l) l)))

put-nth-appendtheorem

(defthm put-nth-append
  (equal (put-nth n v (append a b))
    (if (< (nfix n) (len a))
      (append (put-nth n v a) b)
      (append a (put-nth (- n (len a)) v b)))))

local

(local (defun put-nth-firstn-induction
    (i j l)
    (declare (xargs :guard (and (true-listp l)
          (integerp i)
          (<= 0 i)
          (integerp j)
          (<= 0 j))))
    (cond ((endp (firstn j l)) 0)
      ((zp i) 0)
      (t (put-nth-firstn-induction (1- i) (1- j) (cdr l))))))

put-nth-firstntheorem

(defthm put-nth-firstn
  (equal (put-nth i v (firstn j l))
    (if (< (nfix i) (nfix j))
      (firstn j (put-nth i v l))
      (firstn j l)))
  :hints (("Goal" :induct (put-nth-firstn-induction i j l))))

put-nth-nthcdrtheorem

(defthm put-nth-nthcdr
  (equal (put-nth i v (nthcdr j l))
    (nthcdr j (put-nth (+ (nfix j) (nfix i)) v l)))
  :hints (("Goal" :induct t)))

put-nth-nththeorem

(defthm put-nth-nth
  (implies (true-listp l) (equal (put-nth i (nth i l) l) l)))

put-nth-put-nththeorem

(defthm put-nth-put-nth
  (equal (put-nth j b (put-nth i a l))
    (if (= (nfix i) (nfix j))
      (put-nth j b l)
      (put-nth i a (put-nth j b l))))
  :rule-classes ((:rewrite :corollary (implies (= (nfix i) (nfix j))
       (equal (put-nth j b (put-nth i a l)) (put-nth j b l)))) (:rewrite :corollary (implies (< (nfix i) (nfix j))
        (equal (put-nth j b (put-nth i a l))
          (put-nth i a (put-nth j b l)))))))

remove-equal-non-member-equaltheorem

(defthm remove-equal-non-member-equal
  (implies (and (true-listp l) (not (member-equal x l)))
    (equal (remove-equal x l) l)))

remove-equal-appendtheorem

(defthm remove-equal-append
  (equal (remove-equal x (append a b))
    (append (remove-equal x a) (remove-equal x b))))

remove-equal-remove-equaltheorem

(defthm remove-equal-remove-equal
  (equal (remove-equal y (remove-equal x l))
    (if (equal x y)
      (remove-equal x l)
      (remove-equal x (remove-equal y l))))
  :rule-classes ((:rewrite :corollary (equal (remove-equal x (remove-equal x l))
       (remove-equal x l)))))

update-nth-appendtheorem

(defthm update-nth-append
  (equal (update-nth n v (append a b))
    (if (< (nfix n) (len a))
      (append (update-nth n v a) b)
      (append a (update-nth (- n (len a)) v b)))))

update-nth-nththeorem

(defthm update-nth-nth
  (implies (< (nfix n) (len x))
    (equal (update-nth n (nth n x) x) x)))

update-nth-update-nththeorem

(defthm update-nth-update-nth
  (equal (update-nth j b (update-nth i a l))
    (if (= (nfix i) (nfix j))
      (update-nth j b l)
      (update-nth i a (update-nth j b l))))
  :rule-classes ((:rewrite :corollary (implies (= (nfix i) (nfix j))
       (equal (update-nth j b (update-nth i a l))
         (update-nth j b l)))) (:rewrite :corollary (implies (not (= (nfix i) (nfix j)))
        (equal (update-nth j b (update-nth i a l))
          (update-nth i a (update-nth j b l))))
      :loop-stopper ((j i)))))

true-listp-update-nth-rwtheorem

(defthm true-listp-update-nth-rw
  (implies (true-listp x) (true-listp (update-nth n v x))))

encapsulate

(encapsulate nil
  (local (defun my-induct
      (n m lst)
      (if (zp n)
        (list lst)
        (if (zp m)
          nil
          (my-induct (- n 1)
            (- m 1)
            (if (atom lst)
              lst
              (cdr lst)))))))
  (local (in-theory (enable nth)))
  (defthmd nth-of-resize-list-split
    (equal (nth n (resize-list lst m default-value))
      (let ((n (nfix n)) (m (nfix m)))
        (and (< n m)
          (if (< n (len lst))
            (nth n lst)
            default-value))))
    :hints (("Goal" :expand (resize-list lst m default-value)
       :induct (my-induct n m lst)))))

nth-of-resize-list-preservedtheorem

(defthm nth-of-resize-list-preserved
  (implies (and (< (nfix n) (len lst)) (< (nfix n) (nfix m)))
    (equal (nth n (resize-list lst m default-value))
      (nth n lst)))
  :hints (("Goal" :in-theory (enable nth-of-resize-list-split))))

nth-of-resize-list-too-bigtheorem

(defthm nth-of-resize-list-too-big
  (implies (<= (nfix m) (nfix n))
    (equal (nth n (resize-list lst m default-value)) nil))
  :hints (("Goal" :in-theory (enable nth-of-resize-list-split))))

nth-of-resize-list-newly-in-boundstheorem

(defthm nth-of-resize-list-newly-in-bounds
  (implies (and (<= (len lst) (nfix n)) (< (nfix n) (nfix m)))
    (equal (nth n (resize-list lst m default-value))
      default-value))
  :hints (("Goal" :in-theory (enable nth-of-resize-list-split))))

len-resize-listtheorem

(defthm len-resize-list
  (equal (len (resize-list lst m default)) (nfix m)))

make-list-ac-redeftheorem

(defthm make-list-ac-redef
  (equal (make-list-ac n x acc)
    (if (zp n)
      acc
      (cons x (make-list-ac (1- n) x acc))))
  :rule-classes ((:definition :clique (make-list-ac)
     :controller-alist ((make-list-ac t nil nil)))))

countdown2-indfunction

(defun countdown2-ind
  (n m)
  (if (zp m)
    n
    (countdown2-ind (nfix (1- (nfix n))) (1- m))))

resize-list-of-make-list-ac-sametheorem

(defthm resize-list-of-make-list-ac-same
  (equal (resize-list (make-list-ac n x nil) m x)
    (make-list-ac m x nil))
  :hints (("goal" :induct (countdown2-ind n m)
     :expand ((make-list-ac n x nil)))))

resize-list-when-emptytheorem

(defthm resize-list-when-empty
  (implies (atom lst)
    (equal (resize-list lst n x) (make-list-ac n x nil))))

make-list-ac-indfunction

(defun make-list-ac-ind
  (n x acc)
  (if (zp n)
    acc
    (cons x (make-list-ac-ind (1- n) x acc))))

make-list-ac-inducttheorem

(defthm make-list-ac-induct
  t
  :rule-classes ((:induction :pattern (make-list-ac n x acc)
     :scheme (make-list-ac-ind n x acc))))

in-theory

(in-theory (disable butlast
    position
    position-eq
    position-equal
    occurrences
    occurrences-eq
    occurrences-equal))

Included Books