Locate the last occurrence of a substring.

`(strrpos x y)` searches through the string

The function is "efficient" in the sense that it does not coerce its arguments into lists, but rather traverses both strings with char. On the other hand, it is a naive string search which operates by repeatedly calling strprefixp, rather than some better algorithm.

Corner case: we say that the empty string **is** an prefix of any other
string. As a consequence,

**Function: **

(defun strrpos$inline (x y) (declare (type string x y)) (let ((x (mbe :logic (str-fix x) :exec x)) (y (mbe :logic (str-fix y) :exec y)) (yl (length (the string y)))) (declare (type string x y) (type (integer 0 *) yl)) (strrpos-fast (the string x) (the string y) (the (integer 0 *) yl) (the (integer 0 *) (length (the string x))) (the (integer 0 *) yl))))

**Theorem: **

(defthm strrpos-type (or (and (integerp (strrpos x y)) (<= 0 (strrpos x y))) (not (strrpos x y))) :rule-classes :type-prescription)

**Theorem: **

(defthm prefixp-of-strrpos (implies (strrpos x y) (prefixp (explode x) (nthcdr (strrpos x y) (explode y)))))

**Theorem: **

(defthm completeness-of-strrpos (implies (and (prefixp (explode x) (nthcdr m (explode y))) (<= m (len y)) (force (natp m))) (and (natp (strrpos x y)) (>= (strrpos x y) m))))

**Theorem: **

(defthm strrpos-upper-bound-weak (implies (force (stringp y)) (<= (strrpos x y) (len (explode y)))) :rule-classes ((:rewrite) (:linear)))

**Theorem: **

(defthm strrpos-upper-bound-strong (implies (and (not (equal y "")) (not (equal x "")) (force (stringp x)) (force (stringp y))) (< (strrpos x y) (len (explode y)))) :rule-classes ((:rewrite) (:linear)))

**Theorem: **

(defthm strrpos-upper-bound-stronger (implies (and (strrpos x y) (force (stringp x)) (force (stringp y))) (<= (strrpos x y) (- (len (explode y)) (len (explode x))))) :rule-classes ((:rewrite) (:linear)))

- Strrpos-fast
- Fast implementation of strrpos.