extend-pathname

(local (encapsulate nil
    (local (in-theory (enable make-character-list)))
    (defthm make-character-list-when-character-listp
      (implies (character-listp x)
        (equal (make-character-list x) x)))
    (defthm character-listp-of-make-character-list
      (character-listp (make-character-list x)))
    (defthm len-of-make-character-list
      (equal (len (make-character-list x)) (len x)))))

(local (defthm coerce-inverse-1-better
    (equal (coerce (coerce x 'string) 'list)
      (if (stringp x)
        nil
        (make-character-list x)))
    :hints (("Goal" :use ((:instance completion-of-coerce (x x) (y 'string)))))))

(local (in-theory (disable coerce-inverse-1)))

(local (defthm len-revappend
    (equal (len (revappend x y)) (+ (len x) (len y)))))

(local (defthm len-of-take (equal (len (take i l)) (nfix i))))

(local (defthm length-subseq
    (implies (and (stringp s)
        (natp m)
        (natp n)
        (<= m n)
        (<= n (length s)))
      (equal (length (subseq s m n)) (- n m)))))

(local (defthm length-string-0
    (implies (and (stringp s) (not (equal s "")))
      (not (equal (length s) 0)))
    :hints (("Goal" :use ((:instance coerce-inverse-2 (x s)))
       :in-theory (disable coerce-inverse-2)
       :expand ((len (coerce s 'list)))))))

(local (in-theory (disable subseq length)))