Compares two objects using alphanumeric comparison on component strings and symbols.
(alphanum-obj-< x y) → *
This is the comparison function used for alphanum-sort. It orders objects as follows:
Function:
(defun alphanum-obj-< (x y) (declare (xargs :guard t)) (let ((__function__ 'alphanum-obj-<)) (declare (ignorable __function__)) (cond ((atom x) (if (atom y) (cond ((stringp x) (if (stringp y) (alphanum-< x y) t)) ((stringp y) nil) ((symbolp x) (if (symbolp y) (cond ((equal (symbol-package-name x) (symbol-package-name y)) (alphanum-< (symbol-name x) (symbol-name y))) (t (alphanum-< (symbol-package-name x) (symbol-package-name y)))) t)) ((symbolp y) nil) ((equal x y) nil) (t (alphorder x y))) t)) ((atom y) nil) ((alphanum-obj-< (car x) (car y)) t) ((equal (car x) (car y)) (alphanum-obj-< (cdr x) (cdr y))) (t nil))))
Theorem:
(defthm alphanum-obj-<-transitive (implies (and (alphanum-obj-< x y) (alphanum-obj-< y z)) (alphanum-obj-< x z)))
Theorem:
(defthm alphanum-obj-<-trichotomy (implies (and (not (alphanum-obj-< x y)) (not (equal x y))) (alphanum-obj-< y x)))
Theorem:
(defthm alphanum-obj-<-negation-transitive (implies (and (not (alphanum-obj-< x y)) (not (alphanum-obj-< y z))) (not (alphanum-obj-< x z))))
Theorem:
(defthm alphanum-obj-<-strict (not (alphanum-obj-< x x)))