Built-in axioms and theorems about the total order.
Theorem:
(defthm alphorder-reflexive (implies (not (consp x)) (alphorder x x)))
Theorem:
(defthm alphorder-anti-symmetric (implies (and (not (consp x)) (not (consp y)) (alphorder x y) (alphorder y x)) (equal x y)) :rule-classes ((:forward-chaining :corollary (implies (and (alphorder x y) (not (consp x)) (not (consp y))) (iff (alphorder y x) (equal x y))) :hints (("Goal" :in-theory (disable alphorder))))))
Theorem:
(defthm alphorder-transitive (implies (and (alphorder x y) (alphorder y z) (not (consp x)) (not (consp y)) (not (consp z))) (alphorder x z)) :rule-classes ((:rewrite :match-free :all)))
Theorem:
(defthm alphorder-total (implies (and (not (consp x)) (not (consp y))) (or (alphorder x y) (alphorder y x))) :rule-classes ((:forward-chaining :corollary (implies (and (not (alphorder x y)) (not (consp x)) (not (consp y))) (alphorder y x)))))
Theorem:
(defthm lexorder-reflexive (lexorder x x))
Theorem:
(defthm lexorder-anti-symmetric (implies (and (lexorder x y) (lexorder y x)) (equal x y)) :rule-classes :forward-chaining)
Theorem:
(defthm lexorder-transitive (implies (and (lexorder x y) (lexorder y z)) (lexorder x z)) :rule-classes ((:rewrite :match-free :all)))
Theorem:
(defthm lexorder-total (or (lexorder x y) (lexorder y x)) :rule-classes ((:forward-chaining :corollary (implies (not (lexorder x y)) (lexorder y x)))))
Theorem:
(defthm true-listp-merge-sort-lexorder (implies (and (true-listp l1) (true-listp l2)) (true-listp (merge-lexorder l1 l2 acc))) :rule-classes :type-prescription)