# Ichar<

Case-insensitive character less-than test.

`(ichar< x y)` determines if x is "smaller" than y, but
ignoring case. Our approach is basically to downcase upper-case letters and
then compare the resulting character codes.

Something subtle about this is that, in the ASCII character ordering, the
upper-case characters do not immediately preceede the lower-case ones. That
is, upper-case Z is at 90, but lower-case a does not start until 97. So, in
our approach, the 6 intervening characters (the square brackets, backslash,
hat, underscore, and backtick) are considered "smaller" than letters, even
though in regular ASCII ordering they are "larger" than the upper-case
letters.

### Definitions and Theorems

**Function: **ichar<$inline

(defun ichar<$inline (x y)
(declare (type character x)
(type character y))
(mbe
:logic
(< (char-code (downcase-char x))
(char-code (downcase-char y)))
:exec
(let* ((xc (the (unsigned-byte 8)
(char-code (the character x))))
(yc (the (unsigned-byte 8)
(char-code (the character y))))
(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))))
(< (the (unsigned-byte 8) xc-fix)
(the (unsigned-byte 8) yc-fix)))))

**Theorem: **ichar<-irreflexive

(defthm ichar<-irreflexive
(not (ichar< x x)))

**Theorem: **ichar<-antisymmetric

(defthm ichar<-antisymmetric
(implies (ichar< x y)
(not (ichar< y x))))

**Theorem: **ichar<-transitive

(defthm ichar<-transitive
(implies (and (ichar< x y) (ichar< y z))
(ichar< x z)))

**Theorem: **ichar<-transitive-two

(defthm ichar<-transitive-two
(implies (and (ichar< y z) (ichar< x y))
(ichar< x z)))

**Theorem: **ichar<-trichotomy-weak

(defthm ichar<-trichotomy-weak
(implies (and (not (ichar< x y))
(not (ichar< y x)))
(equal (ichareqv x y) t)))

**Theorem: **ichareqv-implies-equal-ichar<-1

(defthm ichareqv-implies-equal-ichar<-1
(implies (ichareqv x x-equiv)
(equal (ichar< x y) (ichar< x-equiv y)))
:rule-classes (:congruence))

**Theorem: **ichareqv-implies-equal-ichar<-2

(defthm ichareqv-implies-equal-ichar<-2
(implies (ichareqv y y-equiv)
(equal (ichar< x y) (ichar< x y-equiv)))
:rule-classes (:congruence))

**Theorem: **ichar<-trichotomy-strong

(defthm ichar<-trichotomy-strong
(equal (ichar< x y)
(and (not (ichareqv x y))
(not (ichar< y x))))
:rule-classes ((:rewrite :loop-stopper ((x y)))))