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