subseq

(in-package "STR")

(local (include-book "arithmetic"))

(local (include-book "std/lists/take" :dir :system))

(local (include-book "std/lists/nthcdr" :dir :system))

(local (include-book "coerce"))

(in-theory (disable subseq subseq-list))

(local (in-theory (enable subseq subseq-list)))

(defthm len-of-subseq-list
  (equal (len (subseq-list x start end))
    (nfix (- end start))))

(defthm true-listp-subseq-list
  (true-listp (subseq-list x start end))
  :rule-classes :type-prescription)

(defthm stringp-of-subseq
  (equal (stringp (subseq x start end))
    (stringp x)))

(defthm length-of-subseq
  (equal (length (subseq x start end))
    (nfix (- (or end (length x)) start))))

(defthm len-of-subseq
  (equal (len (subseq x start end))
    (if (stringp x)
      0
      (nfix (- (or end (len x)) start)))))