Irreflexive kernel (i.e. strict version) of atj-type-list-<=.
(atj-type-list-< sub sup) → yes/no
Function:
(defun atj-type-list-< (sub sup) (declare (xargs :guard (and (atj-type-listp sub) (atj-type-listp sup)))) (let ((__function__ 'atj-type-list-<)) (declare (ignorable __function__)) (and (atj-type-list-<= sub sup) (not (atj-type-list-equiv sub sup)))))
Theorem:
(defthm booleanp-of-atj-type-list-< (b* ((yes/no (atj-type-list-< sub sup))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm atj-type-list-<-of-atj-type-list-fix-sub (equal (atj-type-list-< (atj-type-list-fix sub) sup) (atj-type-list-< sub sup)))
Theorem:
(defthm atj-type-list-<-atj-type-list-equiv-congruence-on-sub (implies (atj-type-list-equiv sub sub-equiv) (equal (atj-type-list-< sub sup) (atj-type-list-< sub-equiv sup))) :rule-classes :congruence)
Theorem:
(defthm atj-type-list-<-of-atj-type-list-fix-sup (equal (atj-type-list-< sub (atj-type-list-fix sup)) (atj-type-list-< sub sup)))
Theorem:
(defthm atj-type-list-<-atj-type-list-equiv-congruence-on-sup (implies (atj-type-list-equiv sup sup-equiv) (equal (atj-type-list-< sub sup) (atj-type-list-< sub sup-equiv))) :rule-classes :congruence)