Function:
(defun scan-backward-for-non-whitespace (idx x) (declare (xargs :guard (and (natp idx) (stringp x)))) (declare (xargs :guard (<= idx (length x)))) (let ((__function__ 'scan-backward-for-non-whitespace)) (declare (ignorable __function__)) (b* (((when (zp idx)) (length x)) ((unless (mbt (< 0 (length x)))) 0) (idx (mbe :logic (1- (min idx (length x))) :exec (1- idx))) ((when (not (vl-whitespace-p (char x idx)))) (lnfix idx))) (scan-backward-for-non-whitespace idx x))))
Theorem:
(defthm natp-of-scan-backward-for-non-whitespace (b* ((result-idx (scan-backward-for-non-whitespace idx x))) (natp result-idx)) :rule-classes :type-prescription)
Theorem:
(defthm scan-backward-for-non-whitespace-upper-bound (b* ((?result-idx (scan-backward-for-non-whitespace idx x))) (<= result-idx (length x))) :rule-classes :linear)
Theorem:
(defthm scan-backward-for-non-whitespace-finds-non-whitespace (b* ((?result-idx (scan-backward-for-non-whitespace idx x))) (implies (not (equal result-idx (length x))) (not (vl-whitespace-p (char x result-idx))))))
Theorem:
(defthm scan-backward-for-non-whitespace-bound-when-non-whitespace-exists (b* ((?result-idx (scan-backward-for-non-whitespace idx x))) (implies (and (< (nfix nw-idx) (length x)) (not (vl-whitespace-p (char x nw-idx))) (< (nfix nw-idx) (nfix idx))) (and (<= (nfix nw-idx) result-idx) (< result-idx (length x))))))
Theorem:
(defthm scan-backward-for-non-whitespace-gte-than-scan-for-non-whitespace (<= (scan-for-non-whitespace 0 x) (scan-backward-for-non-whitespace (length x) x)) :rule-classes :linear)