Case-insensitive string less-than test.

`(icharlist< x y)` determines whether the string

Logically, this is identical to:

(icharlist< (explode x) (explode y))

But we use a more efficient implementation which avoids coercing the strings into lists.

NOTE: for reasoning, we leave this function enabled and prefer to work with icharlist< of the explodes as our normal form.

**Function: **

(defun istr<-aux (x y n xl yl) (declare (type string x) (type string y) (type integer n) (type integer xl) (type integer yl) (xargs :guard (and (stringp x) (stringp y) (natp n) (<= n (length x)) (<= n (length y)) (equal xl (length x)) (equal yl (length y))))) (mbe :logic (cond ((zp (- (nfix yl) (nfix n))) nil) ((zp (- (nfix xl) (nfix n))) t) ((ichar< (char x n) (char y n)) t) ((ichar< (char y n) (char x n)) nil) (t (istr<-aux x y (+ (nfix n) 1) xl yl))) :exec (cond ((= (the integer n) (the integer yl)) nil) ((= (the integer n) (the integer xl)) t) (t (let* ((xc (the (unsigned-byte 8) (char-code (the character (char (the string x) (the integer n)))))) (yc (the (unsigned-byte 8) (char-code (the character (char (the string y) (the integer n)))))) (xc-fix (if (and (<= (big-a) (the (unsigned-byte 8) xc)) (<= (the (unsigned-byte 8) xc) (big-z))) (the (unsigned-byte 8) (+ (the (unsigned-byte 8) xc) 32)) (the (unsigned-byte 8) xc))) (yc-fix (if (and (<= (big-a) (the (unsigned-byte 8) yc)) (<= (the (unsigned-byte 8) yc) (big-z))) (the (unsigned-byte 8) (+ (the (unsigned-byte 8) yc) 32)) (the (unsigned-byte 8) yc)))) (cond ((< (the (unsigned-byte 8) xc-fix) (the (unsigned-byte 8) yc-fix)) t) ((< (the (unsigned-byte 8) yc-fix) (the (unsigned-byte 8) xc-fix)) nil) (t (istr<-aux (the string x) (the string y) (the integer (+ (the integer n) 1)) (the integer xl) (the integer yl)))))))))

**Function: **

(defun istr<$inline (x y) (declare (type string x) (type string y)) (mbe :logic (icharlist< (explode x) (explode y)) :exec (istr<-aux (the string x) (the string y) (the integer 0) (the integer (length (the string x))) (the integer (length (the string y))))))

**Theorem: **

(defthm istr<-aux-correct (implies (and (stringp x) (stringp y) (natp n) (<= n (length x)) (<= n (length y)) (equal xl (length x)) (equal yl (length y))) (equal (istr<-aux x y n xl yl) (icharlist< (nthcdr n (coerce x 'list)) (nthcdr n (coerce y 'list))))))

**Theorem: **

(defthm istreqv-implies-equal-istr<-1 (implies (istreqv x x-equiv) (equal (istr< x y) (istr< x-equiv y))) :rule-classes (:congruence))

**Theorem: **

(defthm istreqv-implies-equal-istr<-2 (implies (istreqv y y-equiv) (equal (istr< x y) (istr< x y-equiv))) :rule-classes (:congruence))